lec(logic equivalence check)--cadence 等价性检查工具理解

本文主要是介绍lec(logic equivalence check)--cadence 等价性检查工具理解，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

1. lec是独立的，不基于任何指定的综合工具。

key point是各个module的输入输出端口、DFF、blackbox等关键点，用于lec检查。

extra unmapped points；只存在一种设计中，要么golden，要么revised。
unreachable unmapped points；无法找到一个可观察点，比如没有功能意义的flop端口。
not-mapped unmapped key points；一般是因为name rule导致的RTL与netlist无法映射成功。（因为map的方式，默认情况，首先是利用name映射，如果不成功就利用function映射）

add notranslate module module_name -library -both

如果想对某个特定module设置为黑盒子。
建议去掉module描述段，改为空module，只定义input、output端口，内容为空。这样做完善，因为不去掉module描述内容，那么output端口的逻辑值可能会被固定，影响lec的验证精度。
利用命令，可以生成一个空module，但是端口方向需要手动修改。

write design <filename> -bbox [-gold | -revised]

report black box

比如大多数unreachable的情况，都是spare flops，就是空闲的触发器。没实际功能意义的触发器。

这个设置很重要，直接影响lec对门级网表进行design analysis，elaboration，RTL construction过程。如果设置不准确，会影响lec对门级网表的识别，导致出现mismatch的错误。

不要使用lec编写脚本；而是推荐用dofile作为lec配置脚本。
可以设置session；
RC(RTL Compiler)支持LEC更好一些。因为RC有命令write_do_lec。但DC+LEC的流程，user guide也有介绍，是可以解决的。
不等价原因一
lec设置的时候，对dft/test_mode没有设置常值；这种情况是因为RTL没有DFT，netlist有DFT，所以无法等价，必须去掉DFT相关的逻辑等价性对比检查。
不等价原因二
一般错误，通过gui界面的diagnosis、不等价点；再通过RTL去分析源代码，很容易debug。
不等价原因三
name rule不一致导致unmapped point，从而产生不等价的结果。注意报告的错误点，其层次路径是否特殊，比如有些generate块，实例名称带[]。这样的RTL和netlist做等价性检查会出不等价的错误。修改lec的name rule就可以解决。
如果是RTL/netlist做lec，那么name rule推荐：
- DC综合+LEC，那么lec的name rule要保持与DC的name rule一致；
- RC综合+LEC，那么lec的name rule要保持与RC的name rule一致；
- 综合和lec里的uniquify命令（命名唯一化），也要保持一致。如果lec和综合工具的name rule一致，并且uniquify的话，按道理讲，RTL与netlist的module名称、instance名称都应该对应起来。

具体解决实例如下图所示：
这里写图片描述

如上方案都解决不了，可以检查代码版本、比较综合的中间网表版本、比较下一层次的网表等方法。
其中，比较综合的中间网表版本，也是一种常见方法。因为综合的中间网表，与RTL和最终网表，map会更容易；lec更容易检查。RTL与综合的中间网表做lec；最终网表与综合的中间网表做lec；两步骤后，可以认为RTL与最终网表是等价的。
比如：DC/RC综合netlist和RTL，做lec检查。
RC和lec属于一家公司，所以切合度很高，容易PASS。
但是DC和lec，有可能会出现问题。这时，可以利用综合的中间版本网表，作为桥梁。也许会有意想不到的debug效果。（Conformal_User.pdf里有专门的DC综合与lec的流程介绍）

参考文档：