为什么形式验证失败
这次项目中发现DC编译后的网表和RTL做形式验证，有两个模块的输出验证失败了。
特地来求教：
1、都是DC家的工具，为什么编译和形式验证会过不了?我原来以为，用自家的工具做形式验证是多余的，因为算法都一样，所以肯定能算出电路是一样的。
2、但是听说retiming会使形式验证失败，是真的吗?
3、形式验证失败后要如何调整?我们用diagnose来看电路，RTL和网表的差别太大了，一时半会看不懂。而代码又是重用公司以前的旧代码，现在也找不到人维护了。
tape out迫在眉睫……要悲剧了……
小问题， 我知道原因，你联系qq： 66399907 我告诉你。
以前也碰到过，后来没办法，直接放过去了。
不知道楼上有身高招，PO出来共享一下吧。
你设计里边有ram或rom没，这两个不能做形式验证，要设置成黑盒
一般用工具，最好是先浏览下工具的手册，知道它能干什么不能干什么，出了问题该怎样debug。
RAM\ROM\还有io-pad都做成黑盒子了。
失败的模块是纯逻辑搭建的，没有使用特定的器件。
现在主要是对形式验证不了解，不知道问题出在哪里。
看来真的要去查手册了。
08年我做过形式验证，现在有些忘了。
复杂的项目，形式验证还是必要的。
形式验证有些常用命令还是比较重要的 建议小编看看用户手册
把DC综合时产生的.svf文件读进来，看看会不会好一些?
svf文件必须要引入的，否则不一致的地方会更多。
有一些状态机或相关的信号在综合后由于某些状态取不到所以被优化了，但是在综合前是所有值都能取到的，这一部分信会导致failing.由其是在跨模块验证时。
似乎还跟DC编译时的优化选项有关。
NND，不管了。
说明你写的rtl有问题
这个是重用模块，之前工程都跑完了，流片都没问题。
6天流片就出来了，成功了。恭喜你。同时膜拜你的速度。
我是说上一次用这个模块的项目，流片回来没有问题。
A file called default.svf is created automatically during compile,which records the "changes" that boundary optimization,register retiming and ungrouping make to the design. This file is readable by Formality,Synopsys'formal verification or equivalency checking tool.