为什么形式验证失败

jackertja

没有接触过后端，对DC也不熟悉。
这次项目中发现DC编译后的网表和RTL做形式验证，有两个模块的输出验证失败了。
特地来求教：
1、都是DC家的工具，为什么编译和形式验证会过不了？我原来以为，用自家的工具做形式验证是多余的，因为算法都一样，所以肯定能算出电路是一样的。
2、但是听说retiming会使形式验证失败，是真的吗？
3、形式验证失败后要如何调整？我们用diagnose来看电路，RTL和网表的差别太大了，一时半会看不懂。而代码又是重用公司以前的旧代码，现在也找不到人维护了。

tape out迫在眉睫……要悲剧了……

voip_winner

小问题， 我知道原因，你联系qq： 66399907   我告诉你。

momooo

以前也碰到过，后来没办法，直接放过去了。。。。
不知道楼上有身高招，PO出来共享一下吧。。

cuichenhust

回复 1# jackertja


    你设计里边有ram或rom没，这两个不能做形式验证，要设置成黑盒


一般用工具，最好是先浏览下工具的手册，知道它能干什么不能干什么，出了问题该怎样debug。

jackertja

RAM\ROM\还有io-pad都做成黑盒子了。

失败的模块是纯逻辑搭建的，没有使用特定的器件。

现在主要是对形式验证不了解，不知道问题出在哪里。
看来真的要去查手册了。

yl5495

08年我做过形式验证，现在有些忘了。

复杂的项目，形式验证还是必要的。

形式验证有些常用命令还是比较重要的  建议楼主看看用户手册

chlor

把DC综合时产生的.svf文件读进来，看看会不会好一些？

yl5495

把DC综合时产生的.svf文件读进来，看看会不会好一些？
chlor 发表于 2011-1-11 15:24

                               
登录/注册后可看大图

    svf文件必须要引入的，否则不一致的地方会更多。

creese

有一些状态机或相关的信号在综合后由于某些状态取不到所以被优化了，但是在综合前是所有值都能取到的，这一部分信会导致failing.由其是在跨模块验证时。

jackertja

似乎还跟DC编译时的优化选项有关。
NND，不管了。