|
|
В базовом SMV есть транслятор в SMV из Synchronous verilog, похожего на verilog язык, который, как я понял, имеет не совсем ту семантику, опасаюсь, что может получиться искажение смысла.
Собираюсь попробовать такую комбинацию:
По спецификации пишется и отлаживается модель с ассертами на SMV.
Другая модель, более близкая к реализации, выполняется на confluence.
Confluence транслируется в SMV и в Verilog (кому нужно, в VHDL).
На confluence написано много ядер и опубликовано на opencores без исходников на нем, но в не очень читабельных файлах на VHDL и Verilog. Можно _надеяться_ на надежную трансляцию. Про надежность трансляции в SMV пока не ясно, посмотрим.
Модель, полученная трансляцией из confluence в SMV проверяется с моделью на SMV.
Теперь текст на confluence можно транслировать в verilog и его использовать как эталон на всех дальнейших этапах работы, проверясь equivalency checker-ами, тем же formality, если он запуститься.
Другой вопрос, а хватит ли checker-ов для достаточно большого проекта, и влезет ли памяти сколько нужно (интересно сколько) в материнскую плату.
|
|
E-mail: 
info@telesys.ru
