RTL2GDS：逻辑等效性检查，LEC

RTL进入流片阶段前，需要经过大量EDA工具的处理。这个过程中真的不会出现任何错误吗？如果工具因错误额外添加了一个反相器，会产生什么后果？

形式验证，尤其是逻辑等价性检查（LEC），已成为现代ASIC设计流程中不可或缺的方法论。

与仿真不同，LEC无需测试向量。它通过静态分析方法，确保两种设计表示形式在数学逻辑层面实现全覆盖等效行为。

LEC的核心目标在于验证设计转换过程的完整性。 当RTL（寄存器传输级）代码经逻辑综合转换为门级网表时，或P&R工具为时序优化修改逻辑时，以及在DFT（可测试性设计）过程中插入扫描链时，该方法可验证原始设计者意图（黄金设计）在修改后的设计（修订设计）中是否得到完整保留。

如上图所示，LEC在多个阶段反复执行：RTL与综合网表对比、综合网表与DFT网表对比，以及最终布局网表验证等。

这相当于一道安全屏障，能即时捕捉各阶段可能出现的工具缺陷或人为操作导致的逻辑错误，从而避免高昂的重新流片成本。

2. 形式验证的数学与算法基础

要理解LEC工具"数学证明"的含义，必须探究其底层的算法原理。LEC工具主要基于二进制决策图（BDD）(BDD)与布尔可满足性（Boolean Satisfiability, (SAT)这两项核心技术。

2.1 Miter电路构造与反驳式验证

LEC的基本原理是通过比较两个电路（参考电路与测试电路），寻找输出存在差异的情况——哪怕仅存在"一个"差异点。为此，工具会构造虚拟的Miter电路。 Miter电路的结构是将两个电路的相同输入端口相互连接，并将对应的输出端口通过异或门连接。

逻辑上，异或门仅在两个输入不同时输出'1'。 因此LEC工具的目标可归结为回答"是否存在使异或门输出为1的输入组合？"这一问题。

• 若存在此类输入组合（反例），则两电路非等价。
• 若所有可能输入下异或输出始终为'0'，则两电路等价。

该方法基于反证法思维：相较于"证明等价"，"寻找差异"在算法层面可能更具效率。

2.2 二进制决策图（BDD）

作为早期LEC工具基础的BDD，是一种将布尔值以有向无环图（DAG）形式表示的数据结构。其最强大的特性在于具备规范形式。

规范形式是指根据输入组合完全展开的逻辑函数标准表达。其含义在于：当特定逻辑函数的变量顺序固定时，表示该函数的BDD图结构具有唯一性。这极大简化了验证过程。

黄金电路与修订电路分别生成BDD后，仅需通过指针比较即可验证两图在内存中是否具有相同结构（即从根节点到终端节点的路径是否一致）。

然而BDD存在致命缺陷——内存爆炸问题。 当涉及乘法器等特定算术运算电路或输入变量众多的复杂逻辑时，BDD的节点数量会呈指数级增长，最终突破物理内存容量限制。这使得基于BDD的验证技术难以处理大规模SoC设计整体。

2.3 可满足性（SAT）求解器

为突破BDD的局限，SAT求解器应运而生。SAT算法旨在探索是否存在能使给定布尔表达式（通常为合取范式CNF）成立的变量赋值方案。

从LEC视角看，SAT求解器旨在寻找使Miter电路输出（异或门）变为'1'的输入条件。与BDD不同，SAT不试图压缩存储整个真值表，而是通过深度优先搜索(DFS)、回溯法 以及学习技术来寻找解法。

• 优点：相较于BDD，内存占用更少，在大规模电路中也能高效运行。 尤其在寻找反例时速度极快。
• 缺点：对于特定问题，搜索空间可能过于庞大，导致求解耗时极长（NP完全问题）。 因此现代LEC工具采用混合方式，结合BDD与SAT技术，或根据电路结构自动选择合适引擎的混合方案。

2.4 逻辑锥分割

将整个芯片视为单个巨型布尔方程进行求解是不可能的。 因此LEC工具将设计分割为Logic Cone的小单元进行验证。

• 比较要点（关键点）：构成验证基准的要素。主要包括主要输出、 Flip-Flop的输入端(D-pin)、Black Box的输入引脚等。
• 逻辑锥的形成：以各比较点为顶点，将所有影响该点的主要输入、触发器输出(Q-pin)、黑盒输出引脚等作为基底，定义组合逻辑区域。

LEC以该逻辑锥体为单位，将原始设计与修订设计进行1:1映射，随后独立验证每对设计是否等价。通过这种"分而治之"方式解决整体问题复杂度。

3. LEC验证流程的具体步骤

在实际工业现场运用Synopsys Formality或Cadence Conformal LEC等工具时，验证流程通常遵循设置、映射、比较、调试的四阶段循环结构。 每个阶段都包含确保验证可靠性的关键细化工作。

3.1 步骤 1：设计建模与设置 - 验证环境的构建

设置阶段是将两个待比较的设计（参考/黄金设计与实现/修订设计）加载到工具中，并构建正确验证环境的过程。 此阶段的细微失误可能导致后续巨大的调试成本，因此需格外谨慎。

1. 库加载 (Library Loading): 加载标准单元库、I/O焊盘库，以及内存或模拟IP等黑盒模型。
   • Synopsys Formality主要采用.db (Synopsys Liberty Binary)格式。
   • Cadence Conformal同时支持.lib（Liberty）格式及仿真用Verilog模型（.v）。关键点在于两类设计必须引用具有相同功能定义的库文件。
2. 设计读取 (Read Design):
   • 黄金设计 (Golden Design): 作为验证基准的设计。通常为RTL（Verilog、VHDL、SystemVerilog）代码。读取RTL时需通过elaborate过程确定参数并生成层次结构。
   • 修订设计：用于对比的参考设计。即综合后生成的网表或布局布线后的网表。
3. 约束设置：
4. 常量设置：网表包含用于测试的扫描链逻辑，其结构与RTL存在差异。因此需将Scan Enable信号固定为0（或非活动值），强制工具仅验证功能路径(Functional Path)。
5. 未驱动信号处理：对于未连接输入端口(Floating inputs)，需定义其应被解释为'0'、 '1'、'Z'（高阻抗状态）或'X'（无关状态）进行定义。错误设置可能导致不必要的验证不一致。

3.2 步骤2：设计映射 - 比较对象的关联

映射是将黄金设计的比较关键点与修订设计的比较点进行1:1对应的过程。在Synopsys工具链中，SVF文件可协助完成此操作。

• 基于名称的映射：当寄存器或端口名称相同或具有规律性模式时使用。 工具默认优先尝试名称匹配。
• 功能映射：即使名称发生变更（例如综合工具在优化过程中随意改名，或数据总线型触发器经多比特触发器分组/解组）， 通过分析驱动该端口的逻辑功能（逻辑锥）相似性尝试映射。该方法计算成本较高，但在验证名称规则被破坏的网表时不可或缺。
• 重命名规则：用户可自定义映射规则。例如当RTL中的reg在网表中变更为reg_0_时， 可指示工具将_替换为``进行映射。
• 未映射点分析：未映射点将被排除在比较对象之外。必须确认这是预期行为（如删除未使用逻辑）还是错误（如命名规则缺失）必须进行确认。

此时将生成未匹配列表。 除LEC失败外，未匹配列表同样需要验证者的分析。

3.3 步骤3：设计比较

映射点对将执行LEC验证。工具采用多阶段策略以实现效率最大化。

• 随机模式模拟：首先注入数千个随机输入模式快速比对输出值。若此阶段出现不匹配，则立即判定为非等价，从而节省高成本的求解器资源。li>
• 结构分析与形式验证： 对通过随机模式测试的节点，启动SAT或BDD求解器尝试进行形式化证明。

结果分为以下四类：

1. 等价：所有输入组合产生相同输出（验证成功）。
2. 非等价：特定输入产生不同输出（设置问题或功能缺陷）。
3. 反转等价：输出完全相反 （例如Q与Qbar的映射）。此类情况在功能上可能等价（允许相位反转时），但需谨慎确认。
4. 中止/结论不明确：工具未能在给定时间或内存限制内完成证明。 这通常发生在具有巨大乘法器等算术逻辑单元或逻辑深度极深的电路中。

3.4 步骤4：调试 - 根本原因分析与修正

比较结果出现非等效或中止时，将进入调试阶段。此阶段最考验LEC工程师的专业能力。 简而言之，当LEC出现失败时，调试过程将异常艰难。

• 诊断：生成引发不匹配的反例，并在逻辑锥体内通过回溯定位错误候选门。
• 模式分析：通过工具提供的波形查看器或原理图查看器，可视化分析信号如何传播至不匹配点。 用户将RTL源代码与网表原理图并列比较，找出逻辑差异。

4. 综合优化与结构转换的处理

LEC验证的最大难点在于RTL与网表在结构上存在显著差异。 逻辑综合工具（Design Compiler、Genus等）为优化面积、功耗和时序，会对RTL的逻辑结构进行大幅改造。若LEC工具无法理解这些结构转换，即使功能完全相同，仍可能判定为不一致（False Negative）。

4.1 组合逻辑优化 (Combinational Logic Optimization)

最基础的优化是运用布尔代数法则进行逻辑简化。

• 常量传播 (Constant Propagation): 当特定输入被固定为常量时，移除或简化相关逻辑。若LEC工具无法识别相同的常量约束条件，可能将其视为错误。
• 逻辑复制与合并：为解决时序问题，可复制扇出数较大的门；反之，为缩减面积，可合并相同逻辑。 LEC工具必须能够处理此类多对一(N:1)或一对多(1:N)映射关系。

4.2 顺序逻辑优化 (Sequential Logic Optimization)

不仅组合逻辑，对寄存器（触发器）本身的变形优化也会使验证更加困难。

• 重定时 (Retiming): 重定时是为缩短关键路径的延迟时间，将寄存器物理移动到组合逻辑对侧的技术。 此时RTL寄存器位置与网表寄存器位置发生偏移，导致无法实现1:1映射。
  • 解决方案：合成工具生成的SVF(SVF)或引导文件必不可少。该文件包含"RTL中的寄存器A已移至网表的寄存器B"等说明信息，使LEC工具可据此重新设置比较点。
  • 详情请参阅Formality® Automated Setup File (SVF)手册中。
  • 但SVF本身也常存在缺陷，有时使用SVF会导致失败，而不用SVF反而能通过。
• 流水线寄存器优化
• FSM重新编码

4.3 层次结构修改

设计层次结构同样属于优化对象。

• 解组 (Ungrouping): 为提高优化效率，综合工具常会打破子模块边界（解组），将其与上级模块合并进行扁平化处理。
  • 问题点:模块边界消失后，将无法进行分层比较，必须将整个设计扁平化后进行比较，导致验证时间激增。此外，submodule/reg可能被重命名为submodule_reg，导致映射失败。
  • 解决方案：应启用自动名称映射功能，或对关键模块在合成时添加set_ungroup false属性以保留层级结构。
• 边界优化 (Boundary Optimization): 指将逻辑移出模块边界（如将逆变器移出模块）或将输入端口的常量向内传播的技术。 此操作同样会在分层比较时引发边界引脚不一致问题，因此需在LEC设置中启用set flatten model -boundary_optimization等选项。

5.低功耗设计中的UPF与LEC

在现代移动及物联网芯片设计中，低功耗技术的应用不可或缺。多电压域与电源门控技术的引入为LEC验证增添了新的复杂性。

5.1 UPF/CPF与电源意图

RTL代码本身不包含电源网络信息。电源域、 隔离、电平转换器等信息则定义在独立文件UPF（统一功耗格式）或CPF（通用功耗格式）中。

进行LEC验证时需同时加载这些UPF/CPF文件。工具基于这些信息在RTL模型中插入虚拟功耗逻辑，从而生成可与实际包含功耗元件的网表进行比对的验证环境。

5.2 低功耗单元验证要点

• 隔离单元：当信号从断电域传导至通电域时，该单元可将信号固定（钳位）为特定值（0或1）。LEC工具会验证UPF中定义的隔离策略（Isolation Strategy）是否在网表中准确实现。若隔离单元缺失或控制信号连接错误，将导致不一致。
• 电平转换器：负责不同电压域间的信号传输。功能上等同于缓冲器，但在LEC中需验证其是否符合电压电平规则。
• 状态保持单元：一种特殊寄存器，可在断电后维持数据。 LEC必须处理普通寄存器与保持寄存器之间的映射，为此必须准确加载库模型。

6. ECO（工程变更指令）与 LEC

在芯片设计的后期阶段，尤其是在布局布线（P&R）或光罩制作前发现缺陷时，通常会执行功能性工程变更指令（FECO）——仅修改最小数量的门电路，而非重新进行整体综合。LEC工具在ECO流程中同样发挥着核心作用。

• 功能ECO：修改RTL后，仅对现有网表添加最小补丁使其与RTL一致的过程。 如Conformal ECO等工具可自动比较修改后的RTL与原网表，生成消除差异所需的补丁逻辑。
• 备用ECO单元应用：当流片已完成且FEOL工艺也已结束时， 需利用芯片内预留的备用门单元（Spare Cells），通过修改BEOL金属层来修复缺陷。LEC工具可接收可用备用单元列表，据此生成最优补丁网表。

结论： 实现无缺陷设计的最后防线

LEC不仅是简单的工具执行流程，更是通过数学手段确保设计完整性的严谨工程程序。在从RTL到门级再到最终布局的漫长设计流程中，尽管会经历无数优化与结构变形，LEC始终作为核心防线，守护着功能本质不受破坏。

要成功运用LEC，必须具备对BDD/SAT等形式化验证理论的理解、对综合及DFT转换过程的深刻认知，以及系统化的调试方法论。随着未来设计规模日益庞大，AI半导体等复杂运算逻辑不断增加，分层验证、顺序逻辑等价性验证(SLEC)、 以及基于云的并行验证等先进技术的重要性将日益凸显。对验证工程师而言，LEC已不再是可选技能，而是必备的生存技能。