EETOP 创芯网论坛 (原名：电子顶级开发网)

标题: [已解决]formality比对内容 [打印本页]

作者: estyzq 时间: 2011-8-9 01:09
标题: [已解决]formality比对内容
本帖最后由 estyzq 于 2012-2-9 19:07 编辑

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

作者: icfbicfb 时间: 2011-8-9 17:25
包括port， gate， net ，connection ，都比较啊
从外到里面，

作者: vampire0322 时间: 2011-8-9 20:59
大大们，为啥reference 和implementl两者调换下位置，一个就是Verification FAILED
另外一个就是Verification SUCCEEDED呢？

作者: estyzq 时间: 2011-8-9 23:02
回复 3# zhq415758192

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

作者: vampire0322 时间: 2011-8-10 09:44
原理大概是这样的
首先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 时间: 2011-8-10 11:37
REF和IMP 调换还有比较结果不一样的，没见过这事情

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

作者: icfbicfb 时间: 2011-8-10 17:48
呵呵，对

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

作者: yuluw2004 时间: 2011-8-17 14:37
回复 10# icfbicfb

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

作者: yue6688 时间: 2021-11-3 16:57

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

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

欢迎光临 EETOP 创芯网论坛 (原名：电子顶级开发网) (https://bbs.eetop.cn/)