[已解决]formality比对内容

estyzq

请问各位高人，formality比较的是网表和rtl中的什么？是比较pins的数量和方向？还是哟很多比较的内容？

icfbicfb

包括port， gate， net ，connection ，都比较啊
从外到里面，

vampire0322

大大们，为啥reference 和implementl两者调换下位置，一个就是Verification FAILED
另外一个就是Verification SUCCEEDED呢？

estyzq

回复 3# zhq415758192


  能否解释下 什么是逻辑一致性？和逻辑锥？

vampire0322

原理大概是这样的
首先formality提取比较节点，包括以下几类：
Primary outputs
Sequential elements
Black box input pins
Nets driven by multiple drivers, where at least one driver is a port or black
box
可以想象，这些节点由其它节点或者input port控制。这些多输入单输出的单元构成一个logic cone，然后比较每一个logic cone。

使用formality时需要的设置不是很多。找一个参考script，把文件和库修改一下后，就可以试着运行了。一般说来，工具能准确地找到compare point，如果有问题，也可以在script中手工指定。跟RTL比较时，还要屏蔽门级设计的scan test部分。

icfbicfb

REF和IMP 调换 还有比较结果不一样的， 没见过这事情

vampire0322

我就遇到过两次哈！如果IMP的逻辑功能和REF相同，但是IMP比REF多几个PORT,Verification SUCCEEDED。而IMP和REF逻辑一致，而REF比IMP多端口，则Verification FAILED。我验证的模块就是多了一个端口，但是两者逻辑关系是等价的。两者调换下位置，就不同的结果。

icfbicfb

呵呵，对

FM 经常出错的， 要具体看下结果就好了，

yuluw2004

回复 10# icfbicfb


    那这样FM就不权威了.
它不出错,不代表没错,
它有错,不代表一定有错,
是这样吗?

yue6688

vampire0322 发表于 2011-8-9 20:59
大大们，为啥reference 和implementl两者调换下位置，一个就是Verification FAILED
另外一个就是Verificat ...

reference 如果较小，implement较大（例如多定义了一些wire），那按照较小的为标准进行比对，大的包含小的，比对成功
如果互换，按照大的为标准，而小的里没有，就比对不过
以上纯属个人见解。