在线咨询
eetop公众号 创芯大讲堂 创芯人才网
切换到宽版

EETOP 创芯网论坛 (原名:电子顶级开发网)

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 8852|回复: 6

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

[复制链接]
发表于 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

Formality结果_20130802.rar

451.54 KB, 下载次数: 73 , 下载积分: 资产 -2 信元, 下载支出 2 信元

发表于 2013-8-11 09:10:58 | 显示全部楼层
svf.....
 楼主| 发表于 2013-8-11 09:19:01 | 显示全部楼层
回复 2# A1985
使用了SVF的,而且报出不等价点的模块中没有看到有rejected的情况。另外,看到一些资料说在读入SVF时被rejected了,可以进行修改svf.txt,但是不知道怎么修改?求教!!!
发表于 2015-5-14 12:34:50 | 显示全部楼层
我先看一下结果怎么样?
发表于 2015-8-5 12:51:08 | 显示全部楼层
see see
发表于 2017-5-17 09:50:28 | 显示全部楼层
下载来看看先
发表于 2022-2-18 15:14:18 | 显示全部楼层
下来看看,谢了!!!!!!!!!!!!!
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

站长推荐 上一条 /2 下一条

×

小黑屋| 手机版| 关于我们| 联系我们| 在线咨询| 隐私声明| EETOP 创芯网
( 京ICP备:10050787号 京公网安备:11010502037710 )

GMT+8, 2024-11-23 03:32 , Processed in 0.021804 second(s), 9 queries , Gzip On, Redis On.

eetop公众号 创芯大讲堂 创芯人才网
快速回复 返回顶部 返回列表