形式验证出错
时间:10-02
整理:3721RD
点击:
使用formality进行RTL代码跟DC之后网表的形式验证,报了40个failing points。我看了下主要是一个叫i_dac_test的信号的不同赋值造成的,该信号是顶层top的一个port。在reference里面i_dac_test由BBOX_NEX的net_drive驱动 值为1,;在Implementation里面i_dac_test就是一个port,值为0。我想知道为何会出现这种情况?该如何解决?谢谢!
个人经验,仅供参考
1, 做eco没有?如果有,不要试图去从failing point来trace , 还是从头看看你的rtl和netlist+eco后有什么区别。
2, 看看mismatch point,看看有什么不对劲的,仔细读读这个log file。
3, 检查你的black box是不是同时被reference和implemente都调用了。
Port 为什么还会有bbox驱动?
1.确定没有做过ECO。
2.report显示REF中有两个 unmatched BBox;但是IMPL中没有unmatched BBox。IMPL中没有任何unmatched points
我也觉得很奇怪啊。目前看来只有REF的这个port由BBox驱动。