3 形式化验证数学基础：核心概念、原理机制、实战要点

RTL 形式化验证之所以能给出“证明”而非“观察”，是因为它把硬件设计与属性都翻译成了数学对象。设计者无需成为数学家，但必须理解验证工具背后的逻辑、模型和判定算法，才能正确选用方法并解读结果。

3.1 问题背景：仿真不够，证明才有确定性

仿真只能证明“测过的那几条路径没有问题”，形式化验证则用数学推理覆盖全部或指定抽象层次的状态空间。

• 验证对象：RTL 模块（Verilog / SystemVerilog）或 SoC 互连协议。
• 验证目标：证明设计满足规约；若不满足，自动给出反例路径。
• 数学语言：逻辑公式、状态机、时序算子。

3.2 核心概念

本章涉及的五个核心概念如下：

• 命题逻辑：布尔变量与 ∧、∨、¬ 运算组成的公式系统，适合描述组合逻辑。
• 时序逻辑：在命题逻辑上增加 X、F、G、U 等时间算子，用于描述状态序列属性（LTL/CTL）。
• Kripke 结构：有限状态系统的标准数学表示 M=(S, I, T, L)。
• 安全属性与活性属性：“坏事永不发生”与“好事最终发生”。
• 验证引擎：SAT 求解器、BDD、不动点计算等判定算法。

3.3 原理机制

形式化验证引擎内部完成一次“数学三连”：

1. 建模（Modeling）：RTL → Kripke 结构 S、I、T、L。
2. 规约（Specification）：设计意图 → 时序逻辑公式（LTL/CTL/SVA）。
3. 判定（Verification）：模型检测器或 SAT/BDD 求解器判断 M ⊨ φ。

若满足，输出 Proof Passed；若不满足，返回一条 反例路径（Counterexample Trace）。

3.4 流程步骤：从 RTL 到证明结果

1. 确定目标类型：等价性检查（EC）还是模型检测（MC）。
2. 构建形式化模型：状态机/事务级模型，必要时做抽象。
3. 编写属性规约：定义安全属性、活性属性或约束条件。
4. 选择验证引擎：BDD、有界 SAT、无界、不动点。
5. 分析结果：证明、反例、超时约束下的有界结论。

3.5 案例说明：4位计数器安全属性验证

待验证设计：4位同步复位计数器，使能时自增。转换后的 Kripke 结构状态为 count 的 16 个取值，初始状态为 0。

用 SVA 和 LTL 描述属性：

// SVA 断言：复位时 count 必须为 0
property p_reset_zero;
  @(posedge clk) rst |-> (count == 0);
endproperty
assert property (p_reset_zero);

// SVA 断言：count 永不超过 15
property p_count_max;
  @(posedge clk) (count <= 4'b1111);
endproperty
assert property (p_count_max);

等价 LTL 公式：G(rst → count = 0) 与 G(count ≤ 15)。

验证引擎穷举 16 个状态及全部迁移，若两条断言均为真，输出 Proof Passed。

3.6 数学概念对照表