DC + Formality : есть ли у DC возможность генерить "guide" для Formality?, один и тот же код синтезированный с разными констрейнами формально раз Опции

[yes]

то есть беру один нетлист в качестве референса, другой имплементайшин

библиотеки общие одинаковые

при этом несовпадающих match point-ов набирается штук 50, и после при verify несколько тыщ несовпадений

-----------------

может нужно какой-то файл для управления Formality сгенерить?


отличия при синтезе - в случае имплементэйшен несколько путей расслаблены - мультисайкл и параметры синтеза и всякие "технологические" констрейны типа max_fanout и т.п. другие
времянка получилась получше, но нет уверенности, что правильно все...

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

[grigorik]

то есть беру один нетлист в качестве референса, другой имплементайшин

библиотеки общие одинаковые

при этом несовпадающих match point-ов набирается штук 50, и после при verify несколько тыщ несовпадений

-----------------

может нужно какой-то файл для управления Formality сгенерить?
отличия при синтезе - в случае имплементэйшен несколько путей расслаблены - мультисайкл и параметры синтеза и всякие "технологические" констрейны типа max_fanout и т.п. другие
времянка получилась получше, но нет уверенности, что правильно все...

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

файл для управления Formality в DC напиши
dc_shell> set_svf design.svf

а потом в Formality напиши
fm_shell(setup)> set_svf design.svf

думаю поможет,

[yes]

файл для управления Formality в DC напиши
dc_shell> set_svf design.svf

а потом в Formality напиши
fm_shell(setup)> set_svf design.svf

думаю поможет,

вряд ли...

этот guidance позволяет отследить преобразование одного нетлиста (или даже вообще RTL - в нетлист только)

а хотелось бы сравнить два нетлиста, полученых после синтеза одного RTL (ну то есть у меня есть два design.svf и два нетлиста, которые я хочу сравнить)

как я понял формалити может считать только инкрементальные svf, ну то есть одно преобразование, затем второе преобразование и т.д., а такие "ветки" как у меня не может
(или я не прав?)

вариант сравнивать с исходным RTL - не подходит, по причине того, что это VHDL код, в котором многие элементы формалитивский ридер не понимает (ну, например, типичный match point, когда индекс массива задается не специальным типом с ранжем==размеру, а интежером)
коллега с этим повозился, но не особо преуспел