形式验证出错

clovis

使用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。我想知道为何会出现这种情况？该如何解决？谢谢！

macdir

个人经验，仅供参考
1， 做eco没有？如果有，不要试图去从failing point来trace ， 还是从头看看你的rtl和netlist+eco后有什么区别。
2， 看看mismatch point，看看有什么不对劲的，仔细读读这个log file。
3， 检查你的black box是不是同时被reference和implemente都调用了。

205207033

Port 为什么还会有bbox驱动？

clovis

回复 2# macdir


    1.确定没有做过ECO。
    2.report显示REF中有两个 unmatched BBox；但是IMPL中没有unmatched BBox。IMPL中没有任何unmatched points

clovis

回复 3# 205207033


    我也觉得很奇怪啊。目前看来只有REF的这个port由BBox驱动。