题记：形式验证在数字电路实现过程中无处不在，从今儿起打算写一系列 LEC 的文章。材料多来自Cadence support 网站的App Note, RAK, Artical.
概述
LEC 全称Logic Equivalence Checking, 是Conformal 家族的长子，关于Conformal 家族成员的介绍请回顾《低调的实力派：Conformal》。形式验证不依赖于输入激励，用数学解析的方式对电路的逻辑等效性做完备验证。在数字电路实现过程中需要对任何做了电路逻辑更改的步骤进行逻辑等效性验证，以确保逻辑的更改不会导致功能的错误。
在数字电路实现过程的众多步骤中，对LEC挑战最大的莫过于逻辑综合，尤其是有复杂运算逻辑的电路。要保证形式验证的独立性，形式验证工具必须具备对复杂电路的建模能力，如对复杂运算逻辑的Operator merging, Advanced Pipeling, retiming, Rsource sharing 等。
运行
LEC 的运行很简单，因为conformal 功能众多，所以LEC 命令有多个option 用于调用不同的license 完成不同的功能，如：
lec -xl -nogui -dofile ./your\_lec\_script.do
其中，-xl 指定需要有运算逻辑分析能力的license；-nogui 指定在起LEC 时不要起GUI，对成熟项目适用，以节省运行时间；-dofile 指定主脚本。
GUI是形式验证debug 的重要手段，对于新手可以直接在GUI 上进行操作，有不熟悉的命令也可以先用GUI 设置然后到log 中找到相应命令。
对于新手而言强烈建议，在进入LEC 后用命令 " set web on -browser " 将内嵌的web interface 打开。这web infterace 里有smaple dofile, 有Guide, 有常见问题，还有工具的feature 介绍。
在数字电路实现过程中，形式验证的对象有两种： RTL2GATE, GATE2GATE. 对于RTL2GATE LEC 有两中flow，hierarchical Comparison flow 和 Flat Comparison flow。因为逻辑综合工具的进步，对于有复杂运算逻辑的电路很难从头到尾一步比过，通常的做法是分两步来比，先比RTL跟中间未对datapath 做ungroup 的netlist, 再比中间netlist 跟最终的netlist. 后续章节将逐步展开。
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/roNiuqGiYwDuyCwGT1bsqQ
作者微信公众号
相关文章推荐
• clock gating | Gating的插入与验证
• clock gating | 从ICG cell 在 library 中的定义说起
更多IC设计技术干货请关注IC设计技术专栏。
