📚 课程目录第3章 Formality工具架构与运行机制

3. Formality工具架构与运行机制

Formality 的等价性验证并不是“把两个网表跑一遍仿真对比波形”，而是一套以形式化数学为基础的静态证明系统。理解它的架构，关键在于看清五条主线：读入与建模、匹配、求解、数据库与命令体系。它们共同决定了“为什么两个设计会被判定为等价，以及为什么有时会给出 Inconclusive”。

一、整体架构：从设计读入到证明结论

Formality 的输入是参考设计（Reference，通常是 RTL 或综合前网表）与实现设计（Implementation，通常是综合后或布局布线后的网表），外加一份指导匹配与求解的脚本。工具内部先把两者转换为统一的内部表示（GTECH 及后续的通用逻辑结构），再进入匹配与求解阶段。整个过程可以概括为：

读入层：解析 Verilog/VHDL/EDIF 等格式，构建设计对象（Design、Instance、Port、Net、Cell）。
建模层：把工艺库单元映射为通用逻辑函数，形成可比较的逻辑锥。
匹配层：在参考与实现之间建立“点对点”的对应关系，包括比较点（Compare Point）与关键点（Key Point）。
求解层：对每个比较点构造 SAT/ATPG 问题，证明其功能等价或找出反例。
数据库层：保存设计、匹配结果、求解状态与调试信息，供后续命令查询。

下图给出 Formality 的架构与数据流关系，重点体现“读入—建模—匹配—求解—数据库”之间的依赖方向，以及命令体系对全流程的控制作用。

二、核心引擎：匹配算法与求解器

匹配算法解决的是“参考中的哪个点，对应实现中的哪个点”。Formality 的匹配是分层的：先按名称匹配（name-based），再按结构匹配（structure-based），最后按功能匹配（function-based）。名称匹配最快，但综合工具常会改名、合并或复制寄存器，因此需要结构匹配来识别相似逻辑锥，功能匹配则借助 SAT 求解判断两个候选点是否功能一致。

比较点（Compare Point）是验证的基本单元，通常包括：

输出端口：顶层输出必须逐一对应。
寄存器（DFF/Latch）：状态保持元件是等价验证的重点。
黑盒边界：未展开的模块端口。
关键点（Key Point）：用户通过 set_compare_point 或 set_dont_verify 显式指定的点。

求解器是 Formality 的“数学心脏”。它把每个比较点转换为一个 SAT 问题：假设参考与实现在该点输出不同，求解器寻找是否存在一组输入使该差异成立。若不存在，则证明等价；若存在，则给出反例（Counterexample），即一组输入向量与对应的输出差异。对于时序电路，求解器还需要处理状态空间，通常采用展开（unrolling）或归纳（induction）策略。

匹配与求解是迭代的：匹配结果影响求解规模，求解失败的反例又可能提示匹配错误。因此实际流程中常先 match 再 verify，根据报告回头调整匹配约束。

三、数据库：设计、匹配与状态的统一存储

Formality 内部维护一个统一的数据库，保存设计对象、匹配关系、求解状态与调试信息。数据库的价值在于：所有命令都围绕同一份数据操作，避免重复读入与重复建模。常用查询命令包括：

report_designs：列出已读入的设计。
report_matched_points：查看匹配成功的比较点。
report_unmatched_points：查看未匹配点，是排障的第一入口。
report_failing_points：查看求解失败的点及反例。
report_status：查看整体验证状态。

数据库还保存了“黑盒”“不验证点”“常量传播”等用户约束。这些约束会直接改变求解器的搜索空间，因此修改约束后必须重新 verify，不能只依赖旧结果。

四、命令体系：从读入到验证的脚本骨架

Formality 使用 Tcl 风格的命令体系，典型脚本骨架如下：

# 1. 读入参考设计与实现设计
read_verilog -container r -libname WORK ref.v
read_verilog -container i -libname WORK impl.v

# 2. 设置顶层与链接
set_top r:/WORK/top
set_top i:/WORK/top
link

# 3. 匹配
match

# 4. 验证
verify

# 5. 报告
report_status
report_unmatched_points
report_failing_points

其中 -container r 与 -container i 分别指定参考与实现容器，这是 Formality 区分两个设计的基本机制。若省略容器，工具可能把两个设计混在同一命名空间，导致匹配混乱。

五、运行机制中的关键判断

实际运行中，最常见的三类结果与判断依据如下：

结果	含义	典型原因	下一步动作
Succeeded	所有比较点均证明等价	匹配正确、约束合理	归档报告，确认覆盖率
Failed	存在反例，功能不等价	RTL 与网表逻辑差异、约束错误	查看反例波形，定位差异逻辑锥
Inconclusive	求解器无法判定	状态空间过大、黑盒未处理、匹配缺失	增加约束、展开黑盒、调整匹配

需要特别注意的是，Inconclusive 不等于失败，也不等于通过。它表示求解器在给定约束与资源下无法给出结论。工程上应优先处理 Inconclusive，因为它往往隐藏着未匹配点、未展开黑盒或过于宽松的 set_dont_verify 约束。

不要用 set_dont_verify 掩盖真实差异。该命令会跳过指定点的验证，若滥用会导致“假通过”。使用前应确认该点确实无需验证，并在报告中记录原因。

六、架构视角下的排障顺序

当验证结果异常时，建议按“数据库查询 → 匹配 → 求解”的顺序排查：先看 report_unmatched_points 是否有大量未匹配点；再看 report_failing_points 的反例是否指向同一逻辑锥；最后检查黑盒、常量传播与不验证点约束。匹配问题通常表现为“大量点未匹配”或“匹配到错误对象”，而求解问题则表现为“匹配正常但反例集中在少数点”。