formality比对内容

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

逻辑一致性对比

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

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

就是真值表一样

原理大概是这样的
首先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部分。

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

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

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

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