|
马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?注册
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 |
|