LEC flow 分flat comparison flow 和 hierarchical comparision flow. 通常RTL2Gate 用hierarchical flow, Gate2Gate 用flat flow. 两种flow 除了compare 命令有差别之外，前面的设置跟后面的分析基本一致，今天先介绍Flat comparison flow.
Flat comparison flow
大多数数字实现流程都可以切分成三步：输入、执行、输出，LEC 同样不例外，就LEC 自身的模式而言， 又分为setup mode 跟 LEC mode, 通过命令set\_system\_mode lec/setup 进行模式切换。setup mode 读入输入文件，设置用户约束，设置modeling; 设置完成后，执行set\_system\_mode lec 切入到LEC 模式，默认工具会在切到LEC 模式时自动做mapping; mapping 完之后，如果所有的key point 都被正确map 就可以进行compare. Compare 后如果有NoN-Eq, Abort 的点，需要进行Diagnose, debug; 如果所有key point 都相等，则LEC 完成。
Input
在做形式验证时，不需要比对RAM, ROM, Analog, Hard IP 内部的逻辑，这些block 内部的逻辑通过其他方式保证功能的正确性，不属于形式验证管辖范畴。所以在读入design 之前可以用如下命令将其设成black box (black box 是LEC 中非常重要的一类object, 许多的不等都可能由black box 引起):
add notranslate module *ram* –library –both
LEC 的输入比较简单，只需要function 描述完整的 .lib （也可以读入仿真模型）跟Golden 侧的RTL 或netlist 和Revised 侧的RTL 或netlist 即可。
add search path /user1/rtl/ -golden
read design *.v –verilog –golden
add search path /user1/verilog/ -lib -revised
read library library.v -verilog –revised
read design revised.v –verilog –revised
Design Constrints
设计约束由用户决定是否加入，用于控制逻辑的行为。LEC 中在读入library 跟design 之后就可加入，LEC 中有多种约束命令用于不同的场景，此处列出常用的几个：
Exclude sections of a design from verification
add pin constraint 0 scan\_en -revised
add instance constraint 0 U1 –revised
Specify behavior, such as one-hot or one-cold.
add net constraints one\_hot my\_out -revised
Specify relationships, such as pin equivalence.
add pin equivalence CLK –invert CLK\_n -revised
Constrain internal nets, such as primary input, primary output, and tied signals.
add primary input SI -module *FSD* -library -both
add tied signal 0 GND -net –revised
set undriven signal 0 –revised
Constrain instances, such as instance equivalence
add instance equivalence my\_reg my\_reg\_rep1 -golden
Constrain feedback.
add cut point /U1/net1 -revised
Modeling Directives
LEC 不依赖于综合工具吐出的guide 文件，Mapping 跟Compare 都依靠内部算法独立进行。LEC 给用户留有Modeling 设置接口，通过Modeling 接口，用户可以告诉LEC，在综合过程中，综合工具都做了哪些事情，如：是否做了clock gating, 是否做了寄存器merge, 是否对常值寄存器做了常值替换等；用户根据相应的综合策略用命令set\_flatten\_model 设置相应的Modeling directives, LEC 根据相应的设置对RTL 建模。Modeling Directives 有很多，会单独介绍，此处只例几个常用设置。
Clock gating
set flatten model –gated\_clock
Sequential constant
set flatten model –seq\_constant
Sequential merging
set flatten model –all\_seq\_merge
Sequential redundant
set flatten model –sequential\_redundant
Switching to LEC Mode
用户约束跟modeling directives 都必须在setup mode 设置，如果不知道某个命令用在哪个模式，可以在LEC 命令行"man" 这个命令，如 man add noblack box , 在最后一行可以看到"setup mode", 说明这个命令只能用在setup mode. LEC 有setup 跟LEC 两个模式，有些命令只能用在setup/LEC 模式，也有命令在两种模式都能使用。
通常，在setup mode 读入库跟设计，做完约束跟modeling 设置之后就可以切到LEC 模式了，命令是"set system mode lec ", 执行这条命令时，LEC 后台会完成以下三件事：
- Golden and Revised designs are flattened.
- Circuit modeling is performed.
- Automatic key point mapping take places after circuit modeling.
Mapping 是切到LEC mode 工具自动完成的动作，如要做额外的mapping 可以用命令map key point 来完成。在切到LEC mode后，可以打开LEC 的第一个debug 利器mapping manager 来查看mapping 的结果。
Comparison
所有key point 都被正确mapping 之后就可以做比较了，在LEC 里执行命令："add compare points" 和 "compare". Compare 的对象是map 好的key point, LEC 中的key point 指逻辑锥的sink points. 包括：primary output, DFFs, DLAT, BBOX, CUT point, Z gate, E gate.
Compare 结束之后同样打开mapping manager, 在最下面一块区域即是compare 的结果，可以进一步分析结果及debug.
Reference Script
在现在主流方法学上，形式验证都分为 Map + compare 两步，形式验证的debug 针对这两步单独进行，后续章节会分别对其进行详细介绍。本文到此为止，以下是参考脚本：
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/qnBRSmenT1ppmx6XtScWIQ
作者微信公众号
相关文章推荐
• clock gating | Gating的插入与验证
• clock gating | 从ICG cell 在 library 中的定义说起
更多IC设计技术干货请关注IC设计技术专栏。
