T27.AI

Блог

Вещественное значение не должно проходить через целочисленный контейнер

2026-08-31 · 7 мин чтения

Смерженная правка генератора Verilog перевела один симуляционный сценарий с 5 PASSED / 6 FAILED на 11 PASSED, а синтаксическая приемка осталась на 380 файлах — поэтому гейты формы и численного смысла должны быть раздельными.

[измерено] Смерженное изменение в t27 нашло два места, где вещественный результат проходил через целочисленный контейнер в генераторе Verilog. В specs/trinet/etx.t27 при icarus-simulate целевой прогон изменился с 5 PASSED / 6 FAILED и кодом выхода 1 на 11 PASSED и код выхода 0.

Файл был допустимым, вычисление — нет

В одном месте каждое умножение отправлялось в __mul_noop, чьи входы [63:0] округляли вещественный операнд до использования. Поэтому __mul_noop(0.3, 10.0) выдавал 0, а ewma_step(5.0, 0.3, 10.0) возвращал 5.0 вместо 6.5. В другом месте любой binding given объявлялся как reg [63:0], поэтому ewma_step(0.5, 0.5, 1.0) сохранял 1 вместо 0.75.

icarus-simulate specs/trinet/etx.t27
до:    5 PASSED / 6 FAILED, код 1
после: 11 PASSED, код 0

[измерено] Изменились 46 из 581 сгенерированных Verilog-файлов. При этом iverilog -g2012 принял 380 файлов и до, и после. Неизменный счёт синтаксически принятых файлов — главное наблюдение: симулятор может принять файл, хотя сгенерированная программа вычисляет другое значение.

Нужны две проверки, а не одна

Синтаксически допустимый сгенерированный файл не доказывает корректность его численного результата.

Поправка сохраняет и отрицательный результат. Тесты убили пять мутаций этого дефекта, но это свидетельство о данном наборе тестов, а не сертификат всего компилятора. Неизменный счёт принятия iverilog также не доказывает вычислительную эквивалентность.

Что остаётся открытым

• Корректность всех вещественных операций, всех спецификаций и каждого бэкенда не установлена.
• Скорость, площадь FPGA, энергия и качество модели после квантования не измерялись.
• Тип Verilog real предназначен только для симуляции; результат icarus-simulate не является результатом синтеза.
• Пять убитых мутаций показывают, что выбранные тесты ловят эти варианты, но не доказывают, что невидимые варианты не выживут.

В инженерном конвейере держите гейты раздельно: один спрашивает, принял ли симулятор сгенерированный файл, другой сравнивает численный результат с независимым ожидаемым значением. Гейт формы проверяет структуру, гейт смысла — вычисление.

Поработаем вместе

Хотите так же проверить собственный дизайн?

Я аудирую RTL и строю независимые побитово точные модели, затем провожу результат через синтез и, когда это полезно, проверяю на плате Artix-7. Первый модуль проверки — бесплатно.

Обсудить задачуУслуга верификации