📚 课程目录第2章等价验证基础与Formality定位

2. 等价验证基础与Formality定位

等价性到底在比较什么

在数字设计流程中，“等价”并不是指两个电路在晶体管级完全一致，而是指它们在可观测行为上一致。形式化地说：对于任意合法的输入序列和任意时刻，如果两个设计在相同初始条件下，其所有输出端口以及被指定为“比较点”的内部寄存器/端口在每个时钟沿后的取值都相同，则称这两个设计等价。这里的关键词是“可观测”和“比较点”——等价验证并不要求内部结构相同，只要求外部可见行为一致。

因此，等价验证的输入通常包含三部分：参考设计（Reference，通常是RTL）、实现设计（Implementation，通常是综合后的门级网表）、以及一份映射关系（Mapping），告诉工具哪些点应该被比较。缺少映射，工具无法知道RTL中的信号data_reg[7:0]对应门级网表中的哪根线，等价检查就无从谈起。

形式验证的分类与Formality的位置

形式验证是一个大范畴，按验证目标可分为几类：等价性检查（Equivalence Checking）、模型检查（Model Checking）、定理证明（Theorem Proving）以及属性检查（Property Checking）。等价性检查又分为组合等价检查和时序等价检查。Formality属于时序等价性检查工具，它通过匹配两个设计的比较点，并对每个比较点建立“锥形逻辑”（Cone of Logic），再用SAT/BDD等引擎证明两个锥形逻辑在功能上等价。

与仿真不同，等价验证是穷举式的：它不依赖测试向量，而是对所有输入组合进行数学证明。这意味着一旦通过，就不存在“漏测”的角落；但同时也意味着它对设计状态空间和映射质量非常敏感。

Formality 在流程中的角色

在典型的 RTL-to-GDSII 流程中，Formality 通常出现在两个关键节点：综合后和布局布线后。综合后验证 RTL 与门级网表的功能一致性，确保综合工具没有因优化、重定时或资源共享而改变设计行为；布局布线后验证网表在插入时钟树、缓冲器、扫描链之后功能是否仍然一致。这两个节点之间，设计可能经历多次优化和修改，每次修改后都应重新运行等价验证。

Formality 的工作流程可以概括为：读入参考设计与实现设计 → 建立比较点映射 → 对每个比较点构建锥形逻辑 → 用 SAT 引擎证明等价性 → 输出 Pass/Fail/Unmatched 报告。其中映射是最关键也最容易出问题的环节。如果映射错误，工具可能报告“不等价”，但实际设计是正确的；反之，如果映射遗漏了某些比较点，则可能漏掉真正的功能错误。

等价验证与仿真的互补关系

仿真和等价验证不是替代关系，而是互补关系。仿真可以验证设计在特定场景下的行为，包括时序、协议、功耗等动态特性；等价验证则专注于“功能是否被改变”这一静态命题。仿真可能因为测试向量覆盖不足而漏掉角落错误，等价验证则不受测试向量限制，但它只能验证“两个设计是否等价”，不能验证“设计是否符合规格”。换句话说，等价验证回答的是“综合有没有改坏”，而不是“设计本身对不对”。

因此，在实际项目中，通常先用仿真验证 RTL 功能正确性，再用 Formality 验证综合和布局布线没有引入功能偏差。两者结合，才能形成完整的验证闭环。

实践提示：运行 Formality 前，建议先检查综合脚本中是否设置了 set_dont_touch、set_dont_use 等约束，这些约束会影响综合优化程度，进而影响等价验证的难度。如果综合时对某些模块做了边界优化，需要在 Formality 中设置对应的 set_boundary 或 set_black_box 处理。

比较点映射的典型操作

在 Formality 中，映射可以通过自动匹配和手动指定两种方式完成。自动匹配依赖命名规则和结构相似性，对于寄存器、端口等通常能自动匹配；但对于综合后重命名的内部信号，往往需要手动指定。例如，RTL 中的 data_reg[7:0] 在门级网表中可能被综合工具重命名为 U1/Z[7:0]，此时需要在 Formality 脚本中显式写出映射关系：

set_mapping -from data_reg[7:0] -to U1/Z[7:0]
set_mapping -from ctrl_fsm/state_reg[2:0] -to U3/state[2:0]

映射完成后，可以用 report_mapping 查看匹配情况，确认没有遗漏或错误匹配。对于未匹配的比较点，工具会标记为 Unmatched，需要逐一排查原因：是命名差异、是综合优化删除、还是设计本身存在差异。

结果判读与常见问题

Formality 的运行结果通常有三种：Pass（等价）、Fail（不等价）、Unmatched（未匹配）。Pass 表示所有比较点均通过等价性证明；Fail 表示至少有一个比较点不等价，需要定位差异锥形逻辑；Unmatched 表示存在未匹配的比较点，需要检查映射或设计完整性。

当出现 Fail 时，Formality 会给出反例（Counterexample），展示一组输入序列使两个设计输出不同。通过分析反例，可以定位到具体的逻辑差异。常见原因包括：综合工具对复位逻辑处理不一致、时钟门控插入导致时序行为变化、未初始化寄存器在门级网表中被优化为常数等。针对这些情况，需要在综合脚本或 Formality 设置中做相应调整，例如设置 set_constant、set_case_analysis 或调整复位策略。

注意：等价验证通过并不代表设计完全正确。它只证明“实现设计与参考设计功能一致”，如果参考设计本身存在功能错误，等价验证无法发现。因此，等价验证必须建立在 RTL 功能验证已经通过的基础之上。

小结

等价验证是数字设计流程中确保综合和布局布线不改变功能的关键手段。Formality 作为时序等价性检查工具，通过比较点映射和锥形逻辑证明，为 RTL 与门级网表之间架起功能一致性的桥梁。理解等价性的定义、形式验证的分类、Formality 的工作流程以及结果判读方法，是后续掌握 Formality 实际操作和调试技巧的基础。