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

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

手机号码,快捷登录

手机号码,快捷登录

找回密码

  登录   注册  

快捷导航
搜帖子
查看: 22942|回复: 31

[求助] RTL与DC出来的netlist 用conformal lec做形式验证可行否?

[复制链接]
发表于 2014-11-3 10:54:00 | 显示全部楼层 |阅读模式

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

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

x
如题,如果是用synopsys的formality,有SVF文件帮助形式验证。用cadence的conformaly要注意什么,我跑的结果是在MAP的时候就说很多不匹配。// Processing Revised ...
// Modeling Revised ...
// Warning: Golden and Revised have different numbers of key points:
// Golden  key points = 13377
// Revised key points = 8410
// Mapping key points ...
// Warning: Golden has 5271 unmapped key points
// Warning: Revised has 373 unmapped key points
================================================================================
Mapped points: SYSTEM class
--------------------------------------------------------------------------------
Mapped points     PI     PO     DFF    BBOX      Total   
--------------------------------------------------------------------------------
Golden            469    979    6514   2         7964   
--------------------------------------------------------------------------------
Revised           469    979    6514   2         7964   
================================================================================
Unmapped points:
================================================================================
Golden:
--------------------------------------------------------------------------------
Unmapped points   DFF    E      Z      BBOX      Total   
--------------------------------------------------------------------------------
Unreachable       92     50     0      0         142     
Not-mapped        130    5136   2      3         5271   
================================================================================
Revised:
--------------------------------------------------------------------------------
Unmapped points   DFF    DLAT   BBOX      Total   
--------------------------------------------------------------------------------
Unreachable       71     2      0         73      
Not-mapped        1      369    3         373     
================================================================================
// Warning: Key point mapping is incomplete
// Running automatic setup...
// Remodeled 6261 gated-clock DFF/DLAT(s) in (R)
// Merged 43 DFF/DLAT(s) in (G)
// Merged 1 DFF/DLAT(s) in (R)
// Modeling sequential merge in (G).
// Modeling sequential merge in (R).
// Automatic setup finished.
发表于 2014-11-4 13:35:52 | 显示全部楼层
我们公司就是用conformal  lec跑的形式验证。
不map有很多原因,我看你golden里有不map的E pin,请问下,你读library的时候是不是需要pad的lib文件?
 楼主| 发表于 2014-11-5 11:26:06 | 显示全部楼层
回复 2# wowyxy3721
不一定需要LIB文件吧,仿真文件也可以。
发表于 2014-11-5 11:40:51 | 显示全部楼层
回复 3# 轻水一杯


   我们有个项目的某block遇到不map的,E pin,当时是把“read_library -liberty”读的lib文件换成了“read_library -verilog”去读.v文件,然后解决了。   其他还没有遇到过E pin的不map。
发表于 2014-11-5 13:22:02 | 显示全部楼层
lec主要用do文件来引导pass ,do文件由rc提供写出,
发表于 2014-11-13 16:07:15 | 显示全部楼层
楼主问题解决了吗?我最近也在研究conformal验证问题,错误与楼主一致,如有解答请告之,非常感谢!!!!
发表于 2016-1-14 17:20:56 | 显示全部楼层
对formality而言,dc会write一个svf文件帮助比较。
对conformal lec而言,也可以用dc 使用report_resource 命令写出一个类似.res的文件来指定data path
在conformal lec使用analyze -data_path .res的命令就可以比对通过。
发表于 2016-11-11 15:49:43 | 显示全部楼层
我在用lec 中加载filelist 中有很多.vp文件 不知道是不是和普通的verilog文件读法一样? 现在老是报告模块没有define ,文件列表和仿真的文件列表是一样的
发表于 2016-12-5 15:21:13 | 显示全部楼层
讚讚讚!
发表于 2017-3-22 14:22:25 | 显示全部楼层
个人经验:
conformal LEC 做验证的时候,一般情况下,如果设置正确,出来的golden和revised file里面的key points的数目不会相差很大,如果很大,可能存在错误,比如有lib没有读全,或者naming rule设置有问题,或者你的RTL读的有问题,比较复杂的是RTL和netlist做对比,netlist和netlist之间一般比较简单些。

做lec一般有两种方法,一种是你在做综合的时候,顺便就生成dofile,以备LEC。另一种就是直接写脚本来做,一般流程是:1,设置golden和revised file ; 2,设置naming rule,blackbox之类;3,读Lib;4,设置约束(dft相关的东西);5,设置system_mode以及compare之类的(R2N和N2N稍有区别);6,产生report。
您需要登录后才可以回帖 登录 | 注册

本版积分规则

关闭

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


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

GMT+8, 2024-12-25 01:46 , Processed in 0.024700 second(s), 5 queries , Gzip On, Redis On.

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