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

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

Существуют Formal Verification тулы, но они предназначены для проверки соответствия RTL и синтезированного из него Nenlist (и то и другое обычно на каком-либо HDL языке). Искать надо у Ментора, Синопсиса и Каденса. Попробовать, думаю стоит, но совсем не факт, что они подойдут к вашему случаю. Если дойдет до экспериментов, то интесесно узнать результаты.

Смотря о какой эквивалентности речь?
Если имеется ввиду функциональная эквивалентность, например когда несколько кусков проекта модифицировались, но при этом функциональность не подлежала(так задумывалось, что не должна была подежать ) модификации , то решение задачи видится в моделировании с максимальным покрытием исходного проекта, а потом в сравнении полученных результатов, это можно сделать в modelsim, active-hdl или любом другом симуляторе, естественно если проект большой задача не из легких.

Вот потому и спрашиваю, что не из легких. 

Вы правильно поняли, именно о модификации и идет речь.

Просто, на мой взгляд проверить, что проект работает так, как он задумывался, намного сложнее, чем проверить, что он работает аналогично другому проекту(могу ошибаться).

Поэтому удивило, что таких утилит нет.

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

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


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

SM:
Огромное спасибо!



Осталось только найти, где это все можно скачать.

Вроде бы, спрашивают про разные проекты, а не про две версии одного и того же...

А в чем разница? Если учесть их формальную эквивалентность? Или Вы никогда не слышали, что бывает так, что вторая версия проекта переписана с нуля и совершенно не узнаваема по сравнению с первой?

тем более, что
подтверждает то, что речь идет о сравнении двух разных версий одного и того же.

Ну да, это все правильно. Просто, des333 вроде бы, не хотел ничего синтезировать... От синтезаторов тоже много чего зависит. Если они разные, то и работать может по-разному, это уж совершенно точно, сам проходил.

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


Скачать - дело за малым - стать своим.
И... Если Вы еще не под линуксом, то мы идем к вам Ибо под винду этого софта нет в природе. Как и очень многого другого, касаемого процесса разработки ПЛИС/ИМС.

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

Хренасе, до чего дошел прогресс....

http://www.synopsys.com/Tools/Verification...ges/ESP-CV.aspx

Это получается можно сравнить эквивалентность описания на верилоге с имплементацией в виде схемы из отдельных транзисторов


pub/EDA/_Synopsys_/fm_vY-2006.06 а новее версии к сожалению пока мимо не проходило.

Ага, только разберитесь сначала какой дистрибутив правильный, а то потом окажется, что под линукс софт(касаемого процесса разработки ПЛИС/ИМС и PCB) глючит значительно значительней чем под винду.

Вы это мне??? Я уже очень давно работаю с разработкой асиков под линуксом, и при первой же возможности ушел туда и с ПЛИСами. Глюков не замечено. Ни со старой FC4, ни сейчас с центос 5.2. А несовместимости - попадались, так это не глюки, и лечатся дибо установкой чего-нить, либо тупым созданием линков туды-сюды.

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

А винда... Место ей на столе у рядового юзера. А у разработчика - разве что для разработки софта и дров под нее, которые этот юзер юзать будет.

Спасибо , просветили!!! Я честно не знал этого до ныне.

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

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

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

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

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

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

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

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

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

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

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