第3章 形式化验证技术栈与工具链：SMT/SAT、模型检验、等价性检查

3.1 问题背景：从动态仿真到形式化验证

IP 模块验证中，动态仿真依赖测试向量激励，覆盖率受限于人为经验与随机样本。对于流水线竞争、总线协议死锁、异常状态跳转等场景，穷举仿真成本极高。形式化验证通过数学推理覆盖全部可达状态或全部输入空间，从“样本观测”走向“全量证明”。

3.2 核心概念：三大技术支柱

• SAT（布尔可满足性）：判断一个布尔表达式是否存在真值赋值，使其结果为真。是后续求解技术的基础。
• SMT（可满足性模理论）：在 SAT 基础上引入位向量、整数、数组、函数等理论谓词，更贴近硬件/软件约束表达。
• 模型检验：对有限状态系统做穷尽探索，验证时序属性、安全性、活性、状态机死锁等。
• 等价性检查：通过 miter 电路将两个设计的等价性问题转化为可满足性问题，再由 SAT/SMT 引擎求解。

3.3 原理机制

3.3.1 SAT/SMT 求解

SAT 求解器基于 DPLL/CDCL 框架：启发式赋值、布尔约束传播、冲突分析、冲突子句学习与重启。SMT 求解器将 SAT 作为布尔骨架，叠加理论求解器处理位向量、整数、数组等约束，从而直接表达 RTL 中的算术与存储逻辑。

3.3.2 模型检验

工业级模型检验通常使用有界模型检验（BMC）与 IC3/PDR 两类方法。BMC 将设计展开为 k 帧，把“性质恒成立”的反例寻找转为 SAT/SMT 求解问题；IC3/PDR 则通过递归提升不变量，逐步推断可达状态集合。若 k 达到系统完备半径，即可给出严格证明。

3.3.3 等价性检查

对两个电路构建 miter：将两个设计的主输入绑定、主输出连接至异或门，若存在输入使得异或结果为 1，则两个设计不等价。等价性检查器把该 miter 电路交给 SAT 引擎，原问题不满足即等价，满足即返回反例。

3.4 形式化验证流程步骤

1. 定义验证目标与属性：安全性、活性、等价性、覆盖性。
2. 准备参考模型：原生 RTL、重构 RTL、参考网表或形式化规范。
3. 建立环境抽象：时钟、复位、扫描链、接口协议约束。
4. 选择验证引擎：等价性检查器、模型检验器、SMT 求解器。
5. 运行验证：设置资源上限、超时、引擎参数与迭代深度。
6. 分析结果：接受证明、定位反例、检查环境约束完整性。
7. 固化回归：将形式化规则和脚本嵌入持续集成。

3.5 案例说明：加法器重构的等价性检查

设计团队将流水线加法器从“串行累加”重构为“树形累加”，需要证明两种 RTL 在输出端口完全等价。等价性检查器命令序列如下：

read_design  original_rtl.v
read_design  revised_rtl.v
set_top      top_module
set_engine   sat
verify

该流程将输出端口等价性转换为 SAT 求解。若返回 Not Equivalent，工具会给出一个反例输入向量；在 IP 模块中，这通常指向进位链编码或中间对齐逻辑不一致，从而逐级定位差异。

3.6 技术对比与工具链

技术	适用验证目标	代表性工具
SAT/SMT	路径约束、时序展开、方程求解、反例生成	MiniSat、Glucose、Z3、CVC5
模型检验	协议属性、有限状态机性质、覆盖证明	Cadence JasperGold、Synopsys VC Formal
等价性检查	RTL 重构、ECO、综合前后网表比对	Cadence Conformal、Synopsys Formality

3.7 误区提醒

• 误区：SAT 只能证明“不可满足”，工程价值有限。实际上无关子句挖掘、不可满足核心和反例轨迹都是调试的关键信息。
• 误区：模型检验可以直接验证任何设计。规模过大或抽象不足时，需要模块划分、等效化简和假设保证推理。
• 误区：等价性检查等于跑一下 formality。成功与否强烈依赖 miter 构造、环境约束、输入假定与黑盒处理。
• 误区：SMT 一定优于 SAT。对纯布尔问题，SMT 的理论调度可能带来额外开销；应根据问题域选择合适理论子集。

3.8 工程实践清单

• 根据任务选择技术路径：重构验证选等价性检查；协议验证选模型检验；路径敏感分析选 SMT。
• 验证前明确时钟、复位、扫描和无关端口，避免虚假反例。
• 为求解器配置合理的超时、内存和迭代上限，保留过程进度日志。
• 反例处理时先检查环境约束完整性，再提取最小反例并定位 RTL 根因。
• 将形式化属性、等价性规则封装为可重用脚本，纳入回归体系。