formality遇到的一点问题

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

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

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

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

只需关注verify

rtl跟综合网表做形式验证有unmatch点是正常的。
出现unmatch点的前提是综合的时候开启了常数寄存器优化或者unload寄存器优化，然后设计冗余的寄存器就会被优化掉
部分比较复杂的被优化掉的寄存器就会报出unmatch，一般情况是需要要前端设计人员确认的，但是一般情况都是没有关系的。
synopsys回复，如果verify比对过了，就说明整个综合过程没有问题，unmatch的寄存器可以不用care

谢谢nidem

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