RTL与DC出来的netlist 用conformal lec做形式验证可行否？

轻水一杯

如题，如果是用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.

wowyxy3721

我们公司就是用conformal  lec跑的形式验证。
不map有很多原因，我看你golden里有不map的E pin，请问下，你读library的时候是不是需要pad的lib文件？

轻水一杯

回复 2# wowyxy3721
不一定需要LIB文件吧，仿真文件也可以。

wowyxy3721

回复 3# 轻水一杯


   我们有个项目的某block遇到不map的，E pin，当时是把“read_library -liberty”读的lib文件换成了“read_library -verilog”去读.v文件，然后解决了。   其他还没有遇到过E pin的不map。

icfbicfb

lec主要用do文件来引导pass ，do文件由rc提供写出，

leebt

楼主问题解决了吗？我最近也在研究conformal验证问题，错误与楼主一致，如有解答请告之，非常感谢！！！！

wuhongyan

对formality而言，dc会write一个svf文件帮助比较。
对conformal lec而言，也可以用dc 使用report_resource 命令写出一个类似.res的文件来指定data path
在conformal lec使用analyze -data_path .res的命令就可以比对通过。

longever

我在用lec 中加载filelist 中有很多.vp文件 不知道是不是和普通的verilog文件读法一样？ 现在老是报告模块没有define ，文件列表和仿真的文件列表是一样的

ngnan

讚讚讚!

ghxy

个人经验：
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。