Верификация процессорного ядра Опции

[flipflop]

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

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

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

[Leka]

Еще надо проверить прерывания/многопоточность и тп - м/б и логические ошибки (на верхнем уровне). У меня, кстати, прерывание реализовано, как аппаратное переключение задачи - проще/лучше делать прерывания через многопоточность, чем многопоточность через прерывания.

И сколько примерно на Спартане/Циклоне ЛУТ/МГц получается для ядра?

[Methane]

Еще надо проверить прерывания/многопоточность и тп - м/б и логические ошибки (на верхнем уровне). У меня, кстати, прерывание реализовано, как аппаратное переключение задачи - проще/лучше делать прерывания через многопоточность, чем многопоточность через прерывания.

Это как? На каждое прерывание/поток по своему набору регистров, конвейеров и всего того что к нему прилагается?

[Leka]

Это как? На каждое прерывание/поток по своему набору регистров, конвейеров и всего того что к нему прилагается?

Что именно дублируется - зависит от архитектуры. Сам конвейер, например, дублировать не нужно. Указатели, программный счетчик, и тп - дублируются. У меня большой регистровый файл (1К слов) на памяти - можно и аппаратно, и софтово (без потери производительности) разграничить память потоков. Софтово даже лучше - железо проще, тактовая выше - для каждого прерывания/потока компилятор создает свои статические переменные (доступны и глобальные). В целом получается проще, чем для "классического" прерывания.

При подключении памяти все падает до 38 МГц

Какой памяти, внешней, или внутренней?

1) Весь дизайн покрывается спецификацией на темпоральной логике (обычно SystemVerilog Assertions).

А "правильность" самой спецификации кто гарантировать будет? Важно не пропустить ошибку, а как локализировать - вопрос религии/бизнеса, имхо.