4. 逻辑等价验证基础

在完成安全属性建模之后，设计者最关心的问题往往是：我写的RTL实现，是否真的与规格书描述的行为一致？逻辑等价验证（Logical Equivalence Checking，LEC）正是回答这一问题的核心技术。它不依赖激励向量，而是通过数学方法穷举所有可能的输入组合，判定两个设计在功能上是否完全等价。理解等价关系的定义、背后的数学基础，以及Jasper如何实现这一过程，是掌握形式验证工具的关键一步。

一、等价关系的严格定义

在形式验证语境下，两个设计M1和M2被称为逻辑等价，当且仅当对于任意时刻t、任意输入序列，两者的所有可观测输出以及内部状态寄存器都保持一致。更形式化地，设两个设计具有相同的输入空间I和输出空间O，若对任意输入序列i∈I*，M1(i) = M2(i)，则称M1与M2等价。

这里需要区分几种常见的等价类型：

• 组合等价（Combinational Equivalence）：仅比较无状态逻辑锥的输出，适用于纯组合电路或寄存器的下一状态逻辑。
• 时序等价（Sequential Equivalence）：考虑寄存器状态和时钟行为，要求两个设计在复位后从相同初始状态出发，经过任意时钟周期后状态与输出均一致。
• 安全属性等价：不仅要求功能一致，还要求两个设计对同一安全属性（如无死锁、无越权访问）的满足情况相同。

在Jasper中，等价验证通常以“参考设计（Golden/Reference）”与“实现设计（Revised/Implementation）”配对进行。参考设计可以是RTL、网表或规格模型，实现设计则是经过综合、优化或手工修改后的版本。

二、等价验证的数学基础

LEC的核心数学工具是miter结构与可满足性求解（SAT）。其基本思想是：构造一个“差异检测电路”，将两个设计的对应输出进行异或（XOR）比较，若存在任何输入使异或结果为1，则说明两者不等价；若该异或条件不可满足（UNSAT），则证明等价。

具体地，对于组合等价，miter的布尔函数为：

miter_output = XOR( M1_output(i), M2_output(i) )
等价性证明目标：miter_output == 0 恒成立
即：UNSAT( miter_output == 1 )

对于时序等价，需要引入状态映射。若两个设计的寄存器数量不同（例如经过重定时或状态编码优化），则不能直接逐位比较。此时Jasper采用寄存器映射（Register Mapping）或状态匹配技术，通过寻找两个设计状态空间之间的双射关系，将等价性问题转化为映射后的miter可满足性问题。

此外，Jasper还支持参数化等价与数据路径等价，利用字级求解器和抽象解释处理宽数据通路，避免位级SAT在宽总线上的爆炸。其数学本质是：在保持可观测行为不变的前提下，对设计进行行为抽象，再在抽象域上判定等价。

三、Jasper中的等价验证实现方式

在JasperGold中，等价验证通过lec命令或check_equivalence流程实现。典型操作步骤如下：

1. 加载参考设计与实现设计：使用read_verilog或read_design分别读入两个版本，并指定顶层模块。
2. 建立映射关系：通过map命令或自动映射，将两个设计的输入、输出、寄存器一一对应。若存在名称差异，需手动指定映射。
3. 设置等价验证模式：选择组合等价或时序等价，指定复位状态和时钟域。
4. 运行验证：执行check_equivalence，Jasper内部构造miter并调用SAT/字级求解器。
5. 分析结果：若返回UNSAT或Equivalent，则证明等价；若返回SAT，则给出反例波形，定位差异。

以下是一个简化的Jasper等价验证脚本示例：

# 读入参考设计与实现设计
read_verilog -golden ref_design.v
read_verilog -revised impl_design.v

# 设置顶层模块
set_top ref_top
set_top impl_top

# 自动映射输入输出与寄存器
map -auto

# 指定复位状态
set_reset -name rst -active high

# 运行等价验证
check_equivalence -mode sequential

# 查看结果
report_equivalence

当两个设计存在寄存器数量差异时，Jasper会自动尝试状态映射。若自动映射失败，设计者需要提供映射文件，明确指定ref_reg与impl_reg的对应关系。对于经过流水线重定时（Retiming）的设计，Jasper还支持时序等价模式，允许寄存器位置移动但保持整体行为不变。

四、等价验证的典型应用场景与结果判读

等价验证在工程中常用于以下场景：

• 综合前后验证：确认综合工具生成的网表与RTL功能一致。
• ECO修改验证：确认工程变更指令（ECO）只影响目标逻辑，未引入意外副作用。
• 低功耗优化验证：确认时钟门控、电源关断等优化未改变功能行为。
• 安全属性保持验证：确认安全防护逻辑在优化后仍然有效。

结果判读时需注意：UNSAT表示等价性成立，但前提是映射正确、复位状态一致、约束完整。若返回SAT，反例波形会显示在哪个时钟周期、哪个输入组合下两个设计输出不同。设计者应首先检查映射是否遗漏或错误，再检查是否存在未约束的输入或未初始化的寄存器。

从工程实践角度看，等价验证的价值在于它提供了“全输入空间”的保证。与仿真不同，仿真只能覆盖有限激励，而LEC通过UNSAT证明覆盖了所有可能。但这也意味着，等价验证的结论完全依赖于约束和映射的正确性。若约束过强，可能掩盖真实差异；若映射错误，可能产生虚假反例。因此，在运行check_equivalence之前，务必确认复位序列、时钟定义、输入约束与设计意图一致。

最后需要强调的是，逻辑等价验证与安全属性验证是互补的。等价验证回答“两个设计是否相同”，安全属性验证回答“设计是否满足安全要求”。在安全关键设计中，通常先做等价验证确认实现与规格一致，再在规格或实现上运行安全属性验证，从而形成完整的验证闭环。