RTL与DC出来的netlist 用conformal lec做形式验证可行否？
// Modeling Revised ...
// Warning: Golden and Revised have different numbers of key points:
// Goldenkey 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 pointsPIPODFFBBOXTotal
--------------------------------------------------------------------------------
Golden469979651427964
--------------------------------------------------------------------------------
Revised469979651427964
================================================================================
Unmapped points:
================================================================================
Golden:
--------------------------------------------------------------------------------
Unmapped pointsDFFEZBBOXTotal
--------------------------------------------------------------------------------
Unreachable925000142
Not-mapped1305136235271
================================================================================
Revised:
--------------------------------------------------------------------------------
Unmapped pointsDFFDLATBBOXTotal
--------------------------------------------------------------------------------
Unreachable712073
Not-mapped13693373
================================================================================
// 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.
我们公司就是用conformallec跑的形式验证。
不map有很多原因，我看你golden里有不map的E pin，请问下，你读library的时候是不是需要pad的lib文件?
不一定需要LIB文件吧，仿真文件也可以。
我们有个项目的某block遇到不map的，E pin，当时是把“read_library -liberty”读的lib文件换成了“read_library -verilog”去读.v文件，然后解决了。其他还没有遇到过E pin的不map。
lec主要用do文件来引导pass ，do文件由rc提供写出，
小编问题解决了吗?我最近也在研究conformal验证问题，错误与小编一致，如有解答请告之，非常感谢！
对formality而言，dc会write一个svf文件帮助比较。
对conformal lec而言，也可以用dc 使用report_resource 命令写出一个类似.res的文件来指定data path
在conformal lec使用analyze -data_path .res的命令就可以比对通过。
我在用lec 中加载filelist 中有很多.vp文件 不知道是不是和普通的verilog文件读法一样? 现在老是报告模块没有define ，文件列表和仿真的文件列表是一样的
讚讚讚！
个人经验：
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。
学习了
你好，DC之后怎么进行lec，网上说是用rc产生do文件，那用DC怎么进行lec，需要怎么样产生do文件，看了楼上的说用report_resources，可是依然不对