跪求各位Formality形式验证的问题

gongxiao · 发表于 2013-8-10 14:38:02

马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

您需要登录才可以下载或查看，没有账号？注册

x

目前我正在用Formality做全芯片的RTL和netlist之间的形式验证，最近的一个版本报出了1731个不等价点，请参见附件，data.log是记录整个FM流程的数据文件； formality.log是FM自动产生的文件；formality_run.fms是脚本文件；report_analysis_results.rpt是使用report_analysis_results命令记录的分析结果文件；report_unmatched_points.rpt是使用report_unmatched_points命令记录的unmatched points的文件。我经过分析估计是以下两类问题造成的：
1、、第一类问题主要在zoomparam这个大模块中，共有1556个不等价点。在终端中运行程序时就出现了带百分比的进度条，可以在data.log中看到如“.............................. 71F/0A/542017P/690595U (43%) 08/6/13 09:54 30743MB/83225.00sec”，这是由于有datapath造成Formality验证得很困难。这个问题以前也一直存在，因此我曾经做过试验，在DC中加入“set_verification_priority zoomparam”命令，以保证形式验证好通过一些，但是当时那个版本做出来并没有让不等价点减少。因此我们将RTL重新进行综合，在DC中仍然使用“set_verification_priority“这条命令，但后面的实例名不再用zoomparam，而是zoomparam更下一层的实例Horz、VertTop、VertBottom，即不等价点所在的实例模块中，请问这样做是否有效果，或者还是其他什么问题造成的？
2、第二类问题主要出现在DDR部分，可以在data.log文件中查看到。首先仍然会出现”............... 1663F/0A/938451P/292569U (76%) 08/6/13 10:51 36801MB/86679.93sec“这样的datapath问题，另外，我使用”analyze_points“命令分析了一下，结果请看report_analysis_results.rpt。我分析DDR部分的不等价应该都是由于在match时出现了unmatched points的情况，进一步分析，出现unmatched points的情况可能是由于DDR中的u_DW_tap实例在综合时被完全打散造成的。举个例，在Ref中，比较点是“Ref BBPin r:/WORK/JM5400/Core_Top/JM5400_DDR/MEMArbitration_two_memphy_async/ddrcontroller_synopsys_0/JM_DWC_DDR3PHY_top/u_DW_tap/tdo”，但是Formality找不到对应的matched points，我自己查找网表，实际上对应的比较点是“Impl DFF i:/WORK/JM5400/Core_Top/JM5400_DDR/MEMArbitration_two_memphy_async/ddrcontroller_synopsys_0/JM_DWC_DDR3PHY_top/u_DW_tap_U10”，而这两点在report_unmatched_points.rpt都能找到，只是没有match上，并且它们的类型也不一样，一个是BBPin，一个是DFF，match不上也属正常。我们检查了一下DC的脚本，使用的是“compile_ultra -no_autoungroup -scan -gate_clock -retime”命令，这样应该能保证网表中模块不会被打散，但是为什么被打散了，是不是因为u_DW_tap这个实例是调用DesignWare库，综合时会被打散造成的？
跪求各位大神的出现，给个提示也好，万分感谢，也可以QQ联系，我的QQ是：18484008