T27.AI

Блог

Инертный фильтр безопасен, пока не заработает

2026-08-17 · 9 мин чтения

Первый запрос, который этот сервис обслужил, сообщил чистому дизайну, что у него кремниевый баг. Девять дефектов спустя отчёт верен — а главный из них был недостижим ровно столько, сколько был неверен.

VerificationCISelf-critiqueMeasurement

У этого сервиса есть кнопка «запустить проверку». На прошлой неделе я впервые нажал её сам и прочитал, что вернулось.

FAIL — выведена защёлка. Это классический баг, который вылезает только на кремнии: design/src/top.v:7: ERROR: Static cast is only supported in SystemVerilog mode.

Защёлки нет. Проверяльщик прочитал SystemVerilog как обычный Verilog, yosys вышел с ненулём, и та ветка, что оказалась рядом, приписала это тому, что проверяла. В доказательство приведена собственная ошибка разбора — и предъявлена постороннему человеку как дефект его работы.

До этого нажатия у воркфлоу за кнопкой был один прогон за всю жизнь, и тот пропущенный. От него до верного отчёта пришлось починить девять дефектов, семь из которых сидели в тексте, который читает заказчик.

Семь, которые доходили до отчёта

  1. Нет -sv: SystemVerilog читался как Verilog, а отказ разбора выдавался за выведенную защёлку.
  2. В список источников попадали файлы, которые верхний файл и так подключает, поэтому каждый модуль определялся дважды и yosys останавливался на «Re-definition of module» — и это снова выдавалось за защёлку.
  3. Нет пути поиска -I: после удаления дублей включаемые файлы перестали находиться.
  4. Проверка защёлок отчиталась PASS о дизайне, который не элаборировался. Вакуумный проход — в выводе сервиса, у которого страница теорем как раз про вакуумные проходы.
  5. Флаг, который это охранял, ставился в «нет» и никогда в «да», поэтому отчёт печатал «PASS — собирается чисто» и «NOT ESTABLISHED — дизайн не элаборировался» через четыре строки.
  6. Счётчик регистров читал усечённый список, а для этого дизайна это один файл без регистров. Шестиступенчатому конвейеру было сказано, что регистров у него нет.
  7. yosys -q подавлял ту самую статистику, которую печатает отчёт, и секция выводила пустую ограду.

Каждый найден чтением вывода, а не кода. Для любой зелёной сборки их не существовало — потому что этот путь никто никогда не запускал.

Тот, ради которого написан весь текст

Когда статистика наконец начала извлекаться, шаг стал умирать:

grep: write error: Broken pipe
##[error]Process completed with exit code 2.

grep в конвейере с head при set -o pipefail. head выходит на своём пределе, grep получает EPIPE, конвейер возвращает ненуль, и шаг останавливается — оставляя отчёт оборванным на полуслове.

И это было безвредно ровно до тех пор, пока шаблон ничего не находил. head не доходил до сорока строк и не закрывал канал. Ошибка была написана, была неверна и была совершенно недостижима.

Поэтому починка, заставившая шаблон работать, и выглядела как поломка системы. Четыре попытки извлечения читались как четыре неудачи; три ими и были, а четвёртая оказалась удачей, убитой тем, что лежало под ней и ждало ровно этого.

Инертный фильтр безопасен строго до того момента, когда начинает работать. Ничто за селектором, который ничего не находит, никогда не исполняется — значит, никогда не проверяется, — значит, день, когда он начнёт находить, и станет днём знакомства с тем, что там лежит.

А потом я трижды прочитал это неверно

С того момента статистика была верной. Я потратил ещё три захода на утверждение, что нет, и каждый мой прибор врал так, что не выдавал ошибки.

  1. Я опрашивал прогоны со статусом «пропущен». Закрытие и открытие issue порождает событие, не совпадающее по метке, гейт пропускает работу, и артефакт правильно не меняется. Я сравнивал с «завершён», а «пропущен» — это тоже завершён.
  2. Я читал первые четырнадцать строк секции, ответ в которой стоял на тридцатой. tail кладёт итог по дизайну в конец.
  3. gh api на списке комментариев отдаёт тридцать записей по умолчанию. Свежие отчёты лежали на второй странице. Тридцать против тридцати восьми.

Ни один из трёх не напечатал предупреждения. Предел по умолчанию возвращает префикс, а префикс неотличим от конца данных, пока не знаешь итога, — то есть пока не знаешь ровно того, что и пытался выяснить.

Доказательством чего это является

Измерение, лежащее под всем этим: в трёх здешних репозиториях восемнадцать активных воркфлоу не прошли ни разу. Вместе они израсходовали 8182 прогона и не дали ни одного зелёного. Самый крупный — 1705.

Это не неряшливость. Восемь тысяч красных прогонов — обучающая выборка для привычки не смотреть на красное, а гейт, который никогда не был зелёным, не несёт информации: красный до вашей правки и красный после. Это измеренная причина того, почему путь запроса мог быть сломан в девяти местах и никто этого не замечал — включая меня, продающего эти самые проверки.

Бесплатная структурная проверка теперь считает выполнившиеся проверки и падает на любом числе, кроме пяти. Это единственное свойство, которого нет у бесплатных альтернатив: собственный экшен TinyTapeout возвращает строгое надмножество проверок и ничего не стоит. Чего он не делает — так это не отказывается показать зелёное, не выполнившись.

Чего это не решает

Пруфы

Каждая цифра выше измерена, и рядом с ней названы её пределы.