Блог
Задача формальной верификации оставалась зелёной всю жизнь, пока три независимых механизма гарантировали, что красной она стать не может: псевдо-синтаксис конфигов, пайп, проверявший tee вместо инструмента, и continue-on-error поверх всего. Путь до первого настоящего доказательства занял семь именованных слоёв — включая RTL на четыре месяца старше тестируемого компилятора и property-файлы, никогда не инстанцировавшие DUT. Финал — первые настоящие формальные вердикты репозитория: fifo и mac, Status PASSED под z3.
Задача формальной верификации была зелёной всю свою жизнь и ни разу не запустила солвер. Ни единого раза. Адверсариальный аудит собственных заявлений нашёл это; путь до первого настоящего доказательства занял семь отдельных слоёв, каждый невидим, пока не вылечен верхний. Вот анатомия — потому что каждый слой — это класс отказа, который живёт и в чужих конвейерах.
Три независимых механизма каждый по отдельности гарантировали зелёный, поэтому починка любого одного не меняла ничего наблюдаемого. Конфиги .sby использовали блоки с отступами, которые инструмент не разбирает, — каждая задача умирала за миллисекунды с ошибкой конфигурации. Условие в шелле было «if sby | tee log» — без pipefail при bash -e условие проверяет код выхода tee, который всегда ноль, так что PASS записывался безусловно, а ветка отказа была недостижимым кодом. И на job'е висел continue-on-error: true — даже упавший шаг не мог сделать прогон красным. Зелёный в квадрате, потом в кубе.
Поймавший это аудит механичен: для каждого зелёного job'а спроси, что реально доказывает его лог, и попробуй опровергнуть утверждение «этот job что-то проверил». Два независимых опровергателя не смогли опровергнуть — находка выжила. Тот же проход нашёл conformance-job, чей вердикт «CLEAN» был статическим полем JSON, отпечатанным в сводку как будто вычисленным, и lint-job, глотавший сообщение «NOT READY — fix parse errors first» собственного инструмента готовности, который печатал вердикт и выходил с нулём.
| слой | что было сломано на самом деле | общий класс |
|---|---|---|
| 1 | псевдо-блоки с отступами в .sby, которые sby читает как мусор | диалект конфига — это контракт; правдоподобный пример — не документация |
| 2 | пути [files], выпрыгивающие через ../../../ из workspace | пути в конфигах резолвятся по правилам инструмента, не по твоим |
| 3 | if sby | tee — условие проверяет tee | при set -e код выхода конвейера — это его последняя стадия; pipefail или потеря каждого вердикта |
| 4 | sby резолвит [files] против cwd вызова, не расположения .sby | запускай инструмент оттуда, откуда его конфиг предполагает запуск |
| 5 | read_verilog без диалектных флагов репо | каждому читателю генерённого кода нужны те же флаги, что и остальному репо |
| 6 | copy-цепочка предпочитала апрельские закоммиченные .v артефакту, сгенерённому минутами раньше в том же прогоне | закоммиченные копии генерённых файлов затеняют молча; свежее первым, протухшее — громко, отсутствие — фатально |
| 7 | property-модули никогда не инстанцировали DUT — assertions висели над не-driven зеркальными портами, в SVA, который инструмент всё равно не разбирает | property-файл, который элаборируется, — ещё не property-файл, который что-то проверяет; инстанцирование DUT — первый assertion |
Слой 6 заслуживает паузы: формальный job тестировал RTL на четыре месяца старше компилятора, который должен был тестировать. А слой 7 — самый глубокий: даже под полноценным SVA-инструментом каждый assertion в тех файлах был вакуумно истинен, потому что порты, которые он ограничивал, не были подключены ни к чему.
Слои с 1 по 4 оплачены по сорок пять минут за урок — по CI-кругу на каждый. Слои с 5 по 7 упали за минуты, потому что вся цепочка инструмента запускается локально без обёртки: yosys prep, write_smt2, yosys-smtbmc с z3 воспроизводят ядро sby точно. Последнее важное правило диагностики: настоящее имя отказа движка живёт в артефакте job'а — per-task logfile.txt, — а лог job'а говорит лишь «engine did not return a status». Скачай артефакт до того, как строить теории.
$ yosys -q -p "read_verilog -formal -sv -DSIMULATION fifo.v; \
read_verilog -formal fifo_formal_props.v; \
prep -top fifo_formal_props; write_smt2 fifo.smt2"
$ yosys-smtbmc -s z3 -t 5 fifo.smt2
## 0:00:00 Status: PASSEDНаборы свойств v1, заменившие висящие, намеренно тонкие: они инстанцируют настоящие сгенерированные модули и утверждают то, что о них сегодня реально доказуемо, — для двух из трёх это единственный инвариант хендшейка, потому что генерённые модули пока не выставляют data-портов вовсе. Тонко, но привязано и доказано: fifo и mac достигают Status PASSED под z3, локально и затем в CI. Первые настоящие формальные вердикты в истории репозитория.
Третий модуль честно запаркован: написание его свойства вскрыло настоящий дефект дизайна — защёлку с комбинационной обратной связью, которую не принимает ни одна SMT-модель; она выведена потому, что кодогенератор опускает записи состояния внутри комбинационного контекста. Property-файл написан, его инвариант кросс-чекнут исчерпывающей симуляцией по всем 256 входным байтам; конфиг несёт суффикс .blocked и номер issue. Запаркованный конфиг с именованной причиной лучше и удалённого, и зелёного.
Зелёный гейт — это утверждение о гейте, а не о дизайне. Единственный способ узнать, который из двух у тебя, — спросить, как выглядел бы красный результат; и если ни один достижимый путь кода не производит красного, зелёный измеряет шелл, а не кремний. Аудить свои зелёные с той же враждебностью, что и красные: сюрпризы хранятся в зелёных.
Каждая цифра выше измерена, и рядом с ней названы её пределы.