在对两个设计做等效性检查的时候，LEC 首先会将两个设计分别切分成由『组合逻辑锥』+ 『KeyPoint』的集合，然后对两个设计中的KeyPoint 做映射匹配， 然后对驱动KeyPoint 输入的逻辑锥进行等效性检查，如果这对KeyPoint 有多个输入，LEC 会分别比较每一个输入的逻辑锥，如果所有输入的逻辑锥等价则这对KeyPoint 相等。
LEC 中的KeyPoint 包括：
- 寄存器 (DFF)
- 锁存器 (DLAT)
- Primary Input (PI)
- Primary output (PO)
- Black box (BBOX)
- TIE-Z (Z gate): 用于表述悬空的pin 或net 及三态门的高阻抗状态
- CUT (CUT gate): 用于表述组合逻辑loop 的断点，或用户设置的cut point.
- TIE-E (error gate): 如果在设计中有X 赋值语句，LEC 默认会将Golden 侧的X 赋值当做Dont care (DC), 会将Revised 侧的X 赋值当做E gate；默认行为对于RTL2Netlist 或netlist2netlist 都适用，如果比的是RTL2RTL 则需要约束工具对Golden 跟Revised 的处理保持一致，需要设置：set x conversion E -both.
LEC 会对所有的KeyPoint 做mapping, 并对每一类KeyPoint 进行分类总结，但并不是所有的KeyPoint 会成为Compare point, 只有满足如下条件的KeyPoint 才会被当做Compare point:
- 必须是被配对(Mapping) 成功的 KeyPoint;
- 必须被组合逻辑锥驱动。
显然，PI, TIE-Z 跟TIE-E 不会被任何组合逻辑锥驱动，所以他们都不会是Compare Point. 但他们会是某些逻辑锥的输入，所以如果这三类KeyPoint 没有被Mapping 上，会影响比较结果。
在做完Mapping 后 LEC 将设计组合成多个由 "KeyPoint + Logic Cone + KeyPoint " 的原子结构，这些『原子结构』即是LEC 的比较对象，每一个『原子结构』都由以下三部分组成：
- Compare point: 组合逻辑锥的EndPoint, 用于捕获逻辑锥的值，它一定是被匹配上的点，即成对的点，单身狗在LEC 世界里是要被消灭的对象。
- Support point: 组合逻辑锥的StartPoint, 它们驱动逻辑锥，给逻辑锥提供输入。
- Combinational logic cloud: 是要被验证的对象，对StartPoint 输入的每一组值进行运算，并产生一组输出到EndPoint。
一个例子：对于这样一个简单的示例，LEC 首先会分别提取Golden 跟 Revised 侧的KeyPoint, 依据前述陈诉，这个示例中的KeyPoint 有：
- PI: A，B, C, CLK
- DFF: FF1, FF2, FF3, FF4
- PO: Q
对于每个KeyPoint 在Golden 跟 Reivsed 侧都有对应的点，所以所有点都可以匹配上，因为PI 没有任何组合逻辑锥的驱动，所以不是Compare Ponit, DFF 跟PO 都是Compare Point, 以FF4对应的『原子结构』为例：
- Compare point: FF4;
- Support point: D pin 的support point 是：FF1, FF2, FF3; CLK pin 的support point 是CLK.
- Combinational logic cloud: 标Logic字样的部分。
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/-fEMFNhSYX0-IPuzK2W5-A
作者微信公众号
相关文章推荐
•Debug | Genus 跟Innvous中cell的命名规则
•大牛访谈：DFT一哥老K
更多IC设计技术干货请关注IC设计技术专栏。
