一种在LEC中识别断点的独特技术可解决中止问题

　　随着设计复杂度越来越高，其中也包含了复杂的数据结构，导致LEC中的中止数量增加，其主要原因在于逻辑等效性检查(LEC)工具在处理复杂逻辑时存在的局限性。中止实际上是形式验证工具无法解决的非确定性结果。其原因在于：

　　i)复杂的数据路径;

　　ii)比较采用大型逻辑锥;

　　iii)大量未关注的细节问题。

　　设计中的中止越多，LEC覆盖率就越低，同时在设计中缺失某些非等效关系的可能性也越大。虽然有多种不同的技术能够解决中止问题，但是都涉及复杂的方法或需要许多手动流程。始终要记住，任何应用的技术都需要具备较短的周转时间、拥有最低的LEC覆盖范围损失并具有对设计者来说非常友好的特性。

　　添加断点是一种避免中止的首选方式，其优势在于不会出现LEC覆盖范围损失。虽然工具自身能够在组合逻辑中的特定点上添加断点，但是大多数时间里这些断点的位置对设计没有帮助。断点的位置对于正确地进行比较和避免出现任何错误的非等效关系说是非常重要的。在层级结构中添加断点实际上将有助于使相同的点出现在RTL和门级网表中。由于LEC分别处理比较元件的输入和输出，因此断点的输入将在LEC比较期间进行验证，并且添加多个断点也不会导致任何问题出现。另外，添加断点会对数据路径进行分区，并允许工具减少数据锥，因此能够解决中止问题。

　　图1(a)说明了整个逻辑都在锁存器(DFlop)输入位置进行比较的传统方法。目前，随着组合逻辑不断增加，以及采用复杂的算法对组合逻辑进行重构，在RTL和门级网表比较的过程中可能会在比较点上出现中止。新的技术需要首先识别被中止的模块，这可以通过运行扁平 LEC完成。一旦识别后，被中止模块边界输入的引脚功能会通过关闭边界反演和允许常数传播经过这些边界输入而被保留。允许常数传播不仅会帮助减少和简化组合逻辑，还可以帮助在面积方面获得更好的QoR。

　　如上图1 (b) 中所示，在被中止模块的边界输入中添加断点，将大型组合云拆分为若干较小的部分。LEC将断点的输入作为比较点来处理，并允许输出的矢量与其对应的比较点进行比较。现在，让我们来比较图1(a)和图 1(b) 之间生成的矢量数量。