什么是Logical Equivalence Checking（形式验证）

IC设计周期分为两个阶段：前端和后端。前端涵盖架构、代码和验证，后端设计涉及在目标技术节点上的物理实现。

design是“以DFF为终点的逻辑块”组成。这些“以DFF为终点的逻辑块”我们把它叫作逻辑锥。逻辑锥是Logical Equivalence Checking的基本单元。

个人理解，检查原理应该跟DFT的test pattern的原理类似，EDA工具应该会假设从input port灌入各种输入信号，在一切正常情况下，每个逻辑锥的输出情况在design修改前后应该是一致的，如果不一致，那就是不等价。

LEC的重要性

Logical Equivalence Checking即逻辑等价性检查（也叫形式验证），简写为LEC。

Design在tape-out之前要经过各种步骤，如逻辑综合、布局&布线、sign-off、ECO和众多优化过程。在每个阶段，我们都需要确保逻辑功能完好无损，并且不会因为任何自动或手动更改而中断。如果在整个过程中的任何时候功能发生变化，整个芯片就会变得毫无用处。这就是为什么LEC是整个芯片设计过程中最重要的检查之一。

随着工艺节点的缩小和芯片复杂性的增加，逻辑等价检查在确保功能的正确性方面发挥着重要作用。

LEC包括三个步骤：Setup Mode, Mapping Mode和Compare Mode。

图1  LEC流程图

有多种 EDA 工具可用于执行 LEC，例如 Synopsys Formality 和 Cadence Conformal。本文以Conformal为例。

LEC的常见步骤

LEC一般包括setup、mapping、compare三个步骤。

Setup

在setup mode下，Conformal 工具读取两个设计。我们指定设计类型，分别是 Golden（综合网表）和 Revised（通常，Revised是 Conformal 工具与 Golden 设计进行比较的修改后网表）。对于 LEC 的执行，Conformal 工具需要三种类型的文件。

.lec 文件引导 Conformal 工具系统地执行不同的命令。

.scan_const 文件提供了与扫描链相关的约束，例如我们是否要忽略此文件中定义的某些scan连接/serdes 输入/输出引脚。

.stdlib 文件包含标准单元库的路径指针，主要是.lib文件，LEC工具可以通过单元库standard cell内部的连接关系。

在从setup mode到 LEC mode的过渡过程中，Conformal 工具对Golden和Revised设计进行展平和建模，并自动map Key point（关键节点）。关键节点定义为：

Primary Inputs

Primary Outputs

D Flip-Flops

D Latches

TIE-E Gates (error gate, created when x-assignment exists in revised design)

TIE-Z Gates (high impedance or floating signals)

Black boxes

mapping

在LEC的第二阶段，Conformal 工具会自动映射关键节点并进行比较。比较完成后，工具会指出差异。Conformal 工具采用两种基于名称的方法和一种无名称方法来映射关键节点。当对逻辑进行了微小更改时，基于名称的映射对于gate-to-gate的比较很有用。

相反，当Conformal工具必须映射具有完全不同名称的设计时，无名称映射方法很有用。默认情况下，当它退出setup mode时，它会自动使用名称优先映射方法映射关键节点。Conformal 工具未映射的关键节点被归类为未映射点（unmapped points）。

未映射的节点分为三类：

额外的未映射点是仅存在于其中一种设计（Golden 或 Revised）中的关键节点。

无法到达的未映射节点是没有可观察点的关键节点，例如primary output。

未映射节点是可到达但在相应设计的逻辑扇入锥中（logic fan-in cone）没有对应点的关键节点。

compare

Conformal 工具映射好关键节点后，验证的下一步是比较。比较检查关键节点以确定它们是等效的还是非等效的。工具比较然后得到compared points是否为：

Equivalent（等效）

Non-equivalent（非等效）

Inverted-equivalent（反相）

Aborted（中止，即没完成compare）

在中止比较点的情况下，我们可以将compare effort更改为更高的设置。因此，Conformal 工具可以仅在中止的比较点上继续比较。Conformal 工具会显示完成的运行时间和用于比较的总内存。

LEC 完成后会生成多个报告：

Non-equivalence report

Unmapped report

Blockbox report

Abort.report

Unreachable.report

Floating.report

Mapped.report

在sign-off或tape out阶段，项目时间可能比较紧，无法处理具有一些严重逻辑故障的block。有时，在进行manual fixes或timing ECO 时，逻辑连接会中断。在物理设计工程师没有太多时间进行block closure的流片阶段出现逻辑故障的可能性很高。此外，当进行functional ECO并进行手动连接时，中断逻辑连接的可能性很高。

案例

首先，如果 LEC 检查Fail，不要惊慌。当 LEC  Fail时，第一步是检查“non-equivalent.report”文件。可能由于某个节点connection断开，导致“non-equivalent.report”文件中报告的单元名称数量较多.

背后的原因是，有许多通过一个断开节点的路径——因此它的所有端点（比较点）——被报告为“Non-equivalent”。

Non-equivalent Report

第一步是check non-equivalent file，下面的non-equivalent file例子显示了在 LEC 中失败的 152 个compare points。

图2 non-equivalent report示例

报告为非等效的这 152 个寄存器是多比特寄存器。合并两个单一寄存器可以成具有多个输入和输出引脚的多位寄存器。例如，如果我们将两个单比特寄存器合并为一个多比特寄存器，它将有 D0、D1 作为输入引脚，Q0、Q1 作为输出引脚。

图3 多比特寄存器合成示意图

由于多毕业寄存器的存在，报告显示 152 个寄存器计为非等效，但实际上只有 72 个是非等效的。由于这些是两位寄存器，因此总数为 72x2=144 寄存器。其余的是单比特寄存器。

Unmapped Report

下一步是检查unmapped file。此文件显示logical connectivity中断的unmapped nets。我们需要trace 这些net并找出这些net的missing connection。

图4 unmapped report示例

在上图中，我们可以看到design中没有map到一个net (BUFT_net_362908)。如图5 所示，一旦我们在 LEC 故障数据库中检查此net (BUFT_net_362908)的 连接，我们会看到它仅连接到其他单元 (*_364714/A) 的输入引脚，但其连接关系 (该驱动cell被无意delete）丢失。

图5 unmapped report中的net

我们可以在版图中看到unmapped report中报告的net的连接关系。

While we do the fanout of net (BUFT_net_362908) which is reported in unmapped file, it is connected to 152 flops in LEC pass database.

我们去trace unmapped report中的该net的fanout情况发现，该net连接到LEC pass的database中对应的152个flop。

这152个flop和non-equivalent report中报告的152个unmapped point是一致的。

现在，我们需要在之前的LEC pass 的database中找到这个net的实际logic connection。在检查时，我们可以很容易地注意到在LEC fail的database中该net的逻辑连接缺少一个反相器。

图6 通过回溯找到unmapped point的正确连接关系

不要混淆un-mapped和non-equivalent reports。在un-mapped report中，我们只看到未驱动输入pin的floating nets，而non-equivalent reports中，我们看到所有作为该missing cell扇出的cell。

修复LEC Issue

找到LEC故障的原因后，我们需要插入一个丢失的反相器，并在LEC fail的database中重新做这个反相器的输入/输出逻辑连接。图 7 显示了新添加的反相器及其输入输出连接。现在，如果我们重新运行 LEC，它将通过，non-equivalent report 将显示零个非等效点。

图7 插入反相器并手动坐好逻辑连接

图8 新的LEC pass

常见导致LEC fail的原因

使用了多比特寄存器。

克隆了寄存器（例如clock gating）。

逻辑连接中断。

Function ECO。

缺少DFT约束。

LEC的好处

减少对后仿真的依赖。

对逻辑综合和布局布线有一个把关作用。

对写的较差的RTL的有一个把关作用。

不需要function test pattern，就可以比较简便地保证功能等价。

降低了后端设计的操作风险。

参考文献

https://solvnet.synopsys.com/dow_retrieve/O-2018.09/dg/forolh/Default.htm#forug/forug1_Verifying_Designs_by_Equivalence_Checking.htm?otSearchResultSrc=advSearch&otSarchResultNumber=3&otPageNum=1

http://www.europractice.stfc.ac.uk/vendors/cadence_encounter_conformal_EC2012_ds.pdf