微波EDA网,见证研发工程师的成长!
首页 > 研发问答 > 微电子和IC设计 > IC后端设计交流 > 形式验证出错

形式验证出错

时间: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驱动。

Copyright © 2017-2020 微波EDA网 版权所有

网站地图

Top