formality遇到的一点问题

孤月飞星 · 发表于 2012-7-27 14:26:34

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

用formality做一个rtl代码与门级网表的形式验证，match的时候出现了一些unmatched点，但是我没有管它，直接往后坐verify，没有failing points。请问出现unmatched points 是什么原因造成的，又该怎么消除这些unmatched points？我在其他网站上看了些资料据说需要match全部通过了才能做后面的verify。

孤月飞星 · 发表于 2012-7-27 14:59:33

怎么没有人说啊，自己先顶一下

205207033 · 发表于 2012-7-27 16:01:47

不需要。综合本身会优化掉些东西，也会插入gating，所以unmatch是必然的。

孤月飞星 · 发表于 2012-7-27 17:23:56

如果 verified 成功了，就算整个形式验证成功了哦

tigerajs · 发表于 2012-7-27 17:45:58

只需关注verify

hunteryhq · 发表于 2012-8-10 17:40:28

rtl跟综合网表做形式验证有unmatch点是正常的。
出现unmatch点的前提是综合的时候开启了常数寄存器优化或者unload寄存器优化，然后设计冗余的寄存器就会被优化掉
部分比较复杂的被优化掉的寄存器就会报出unmatch，一般情况是需要要前端设计人员确认的，但是一般情况都是没有关系的。

synopsys回复，如果verify比对过了，就说明整个综合过程没有问题，unmatch的寄存器可以不用care

我还是不懂 · 发表于 2012-10-6 23:41:47

谢谢 nidem

我还是不懂 · 发表于 2012-10-12 15:56:16

出现这种问题的有可能是 DC版本的问题，我最近使用一个工艺库，只能用高版本的DC综合器，但是怎么调试就是出现不匹配的问题，最后发现是DC综合器的问题，没有管这个我提示，最后做出来流片仿真都能通过～～～

[求助] formality遇到的一点问题

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

相关帖子

站长推荐 /2