Эквивалентность двух схем, Если ли подобные утилиты? Опции

[des333]

Существуют ли программы, позволяющие сравнить функциональность нескольких проектов и сделать вывод об их эквивалентности?

[SM]

Ну елки-палки, как это нету таких программ?

Formality® is an equivalence-checking (EC) solution that uses formal, static techniques to determine if two versions of a design are functionally equivalent. EC tools verify large designs quickly and completely without the use of test vectors. Formality supports all major hardware description languages, database formats, flows, and implementation design optimizations to provide the most comprehensive verification solution available

http://www.synopsys.com/tools/verification.../formality.aspx

И никого не трогает, что сравнивается, netlist vs исходник или исходник1 vs исходник2, или нетлист1 vs нетлист2

особенно не представляю если схемы нарисованы в shematic editor и с использованием генератора готовых ядер (например CoreGenerator в Xilinx ISE)

А что тут представлять-то? Синтезировать, да сравнить нетлисты формальной верификацией.

[yes]

Ну елки-палки, как это нету таких программ?

Formality® is an equivalence-checking (EC) solution that uses formal, static techniques to determine if two versions of a design are functionally equivalent. EC tools verify large designs quickly and completely without the use of test v

....

но вроде бы не позволяет формалити сравнить два независимых дизайна.

все-таки это практический тул, а не эдвансная концепция, он сравнивает только разные шаги одного и того же проекта, да и то если историю модификации, которую пишет DC утерять, то сразу куча точек с расхождениями получится

это не для Вас пояснение - предназначение формалити - проверять, что низкоуровневые оптимизаторы в своей работе не испортили логику (функциональность) проекта, и больше ничего

то есть мне ее заставить сравнить два независимых проекта не удалось (может я не прав)

может SMV
http://www.cs.cmu.edu/~modelcheck/smv.html
или какие-то еще "кудрявые" проекты могут такое делать, но там язык ввода не verilog | vhdl, а специальный язык

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

то есть практически решить задачу эквивалентности произвольных проектов - это симуляция+покрытие(coverage), благо сейчас констрейн-дривен рандом + кавередж это мэйнстрим в верификации...

[SM]

то есть мне ее заставить сравнить два независимых проекта не удалось (может я не прав)

Два полностью независимых я честно говоря не пробовал, а вот два ядра процессора, в которых было совсем по-разному сделанное АЛУ, но типа как эквивалентное, склалось.

Что касается "истории" в DC - это только при boundary optimization важно, когда он инвертирует входы-выходы модулям, а не только переиначивает внутренности, не затрагивая интерфейс. Так как проинвертированный выход модуля это уже не эквивалентный исходному модуль.

[yes]

Два полностью независимых я честно говоря не пробовал, а вот два ядра процессора, в которых было совсем по-разному сделанное АЛУ, но типа как эквивалентное, склалось.

ну там же два шага -
1 ищет точки сравнения,
2 сравнивает функциональность в этих точках

когда я пытался сравнивать проекты с разным происхождением - список несовпадающих точек, для которых сравнение не проводится, по порядку величины совпадало с количеством элементов (типа флип-флопов) в проекте.