Последнюю неделю бьюсь над задачей верификации процессорного ядра (RISC архитектура (load/store), 6 ступенчатый конвейер команд, только целочисленная математика). Задача для меня совсем новая (раньше делал только математику и коммуникационные контроллеры), поэтому не знаю даже с какой стороны подойти.

Пока родилась следующая структура: Есть эталонная модель на SystemC (потактовая, тоже с конвейерными регистрами, но вместо логики обычные C++ методы).
На эталонной модели и верифицируемой RTL-модели прогоняется набор тестовых программ и на каждом такте сверяется содержимое конвейерных регистров. После прогона получаем список команд (а также номер такта и название конвейерного регистра), на которых обнаружены ошибки.

Может ли кто-нибудь поделиться опытом, как на практике верифицируют процессоры и покритиковать мой подход?