Совместите таблицу ожидаемых результатов с локальными инвариантами

Привяжите верификацию к приёму входа

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

Для принятых входов ADD tag10:(250,10) и tag11:(3,5) ожидайте [(10,4,carry1),(11,8,carry0)]. Достоверный, но остановленный выход не удаляет запись. Выдача tag10 удаляет только эту запись. Повторный tag10 или значение 8 с меткой 12 неверны даже при совпадении некоторых чисел. Включайте все значимые флаги и сопутствующие поля.

Локальные инварианты определяют первый ошибочный фронт вместо одного итогового несовпадения. Внутренняя заполненность — count FIFO плюс биты valid ступеней. Добавляйте учёт отмены, если разрешены reset или flush, и используйте одно правило фронта в обоих мониторах.

Совмещайте числовые границы с временными случаями: ноль, максимальные значения, перенос и заём, последовательный трафик, пустые такты, длинные остановки, замена при заполненности и конечное опустошение. Записывайте начальные значения генератора случайных чисел для повторяемых ошибок. По возможности перебирайте малые пространства управления.

Проверки завершения требуют предположения о продвижении и тайм-аута. Когда приёмник постоянно готов, незавершённая работа должна опустошиться. При бесконечных остановках требуйте сохранения и ограниченной заполненности. Намеренное повреждение переноса или задержки метки должно ломать проверки; такой мутационный тест измеряет чувствительность. Успешные модели Node не проверяют соединения HDL, поведение X/Z, пересечение тактовых доменов или временные характеристики реализации. Сообщайте только реально наблюдённую область выполнения.