本文主要是介绍lec(logic equivalence check)--cadence 等价性检查工具理解，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！
文章目录
- 1. lec是独立的，不基于任何指定的综合工具。
- key point mapping
- ummapped points有三类
- formal functional comparison algorithms
- 两种comparison方式
- 2. setup mode 和 lec mode
- 3. blackbox
- set
- report
- 4. unreachable key points
- 设置选项，尽量避免unreachable报告，因为很多情况都是不需要检查逻辑等价性的。
- 5. HDL rule
- 6. 工程debug经验
- 补充（genus15.20.000版本）
- genus有模板脚本
- genus官方文档里推荐两步式lec
- 这篇ppt不错【debug方法参考111~120页码】
1. lec是独立的，不基于任何指定的综合工具。
key point mapping
ummapped points有三类
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映射）
formal functional comparison algorithms
两种comparison方式
- hierachical(gold或者revised，有1个RTL版本的话，适合hierachical)
- flattened（一般用于两个门级设计的比较。）
2. setup mode 和 lec mode
3. blackbox
set
- 例如ram、模拟ip等，设置为黑盒子。不检查内部的逻辑等价性。
add notranslate module module_name -library -both
- 如果想对某个特定module设置为黑盒子。
建议去掉module描述段，改为空module，只定义input、output端口，内容为空。这样做完善，因为不去掉module描述内容，那么output端口的逻辑值可能会被固定，影响lec的验证精度。
利用命令，可以生成一个空module，但是端口方向需要手动修改。
write design <filename> -bbox [-gold | -revised]
report
report black box
4. unreachable key points
设置选项，尽量避免unreachable报告，因为很多情况都是不需要检查逻辑等价性的。
比如大多数unreachable的情况，都是spare flops，就是空闲的触发器。没实际功能意义的触发器。
5. HDL rule
这个设置很重要，直接影响lec对门级网表进行design analysis，elaboration，RTL construction过程。如果设置不准确，会影响lec对门级网表的识别，导致出现mismatch的错误。
6. 工程debug经验
- 不要使用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的流程介绍）
参考文档：
- Conformal_User.pdf
- Conformal_Ref .pdf
- ConformalHDL_Ref.pdf
- cadence LEC_basic.pdf（cadence的PPT,360云盘里）
补充（genus15.20.000版本）
genus有模板脚本
参考
Cadence Genus userguide阅读笔记 - 个人笔记：not for everyone - 博客频道 - CSDN.NET
http://blog.csdn.net/u011729865/article/details/53912787
genus官方文档里推荐两步式lec
利用genus模板，在综合过程中，会产生两个lec脚本文件（相关的genus命令是write_hdl和write_do_lec）。
- rtl2intermediate.lec.do
- intermediate2final.lec.do
分别对应rtl与map后的网表、map后的网表与综合优化后的最终网表。
这篇ppt不错【debug方法参考111~120页码】
http://www.doc88.com/p-9703790400188.html
debug步骤：
- unmapped一定要解决；
- 利用电路视图，显示反标的值，很好追。我记得，lec不能追到根源点，formality能追到根源点，不知道是不是这样，反正formality追到根源点的思路，更适合我，很好用。
这篇关于lec(logic equivalence check)--cadence 等价性检查工具理解的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！
