第3章 模型检查基础：核心概念、原理机制与实战要点

3.1 问题背景

AI 芯片中的 SoC 包含多核缓存一致性协议、NoC 路由仲裁、电源管理状态机等高度并发控制逻辑。传统仿真验证依赖激励驱动，只能覆盖有限输入序列，无法证明系统在全部可达状态下均满足安全属性。模型检查（Model Checking）以穷举状态空间为数学基础，自动判断系统模型是否满足时序性质规格，是协议级与 RTL 控制逻辑验证的核心手段。

3.2 模型检查核心框架

模型检查将验证任务解耦为“系统建模”“性质规格”“引擎求解”与“结果判读”四个部分：

3.3 核心概念

3.3.1 Kripke 结构

Kripke 结构是模型检查对系统建模的标准数学对象：

M = (S, I, R, L)

• S：有限状态集合
• I ⊆ S：初始状态集合
• R ⊆ S × S：状态转移关系
• L : S → 2^AP：原子命题标记函数，标记每个状态下成立的原子命题

3.3.2 时序逻辑

时序逻辑用于描述系统性质。模型检查中两种主流逻辑：

• LTL（线性时序逻辑）：沿单条执行路径描述性质。核心算子：G（恒成立）、F（最终成立）、U（直到）、X（下一状态）。
• CTL（计算树逻辑）：在分支路径上量化描述性质。核心算子：AG、AF、EG、EF。

3.3.3 状态空间

状态空间是系统全部可达状态的集合。模型检查的效率瓶颈直接来自状态空间规模——寄存器数量为 n 时，状态数可达 2^n 量级。

3.4 原理机制

3.4.1 显式状态搜索

从初始状态出发，通过 BFS/DFS 遍历状态图，逐状态检查原子命题是否与规格矛盾。当状态数超过 10^6 时，内存与时间开销急剧上升。

3.4.2 符号模型检查（BDD）

使用二叉决策图（BDD）紧凑编码状态集合与转移关系，通过不动点计算求解可达状态集合。可在秒级处理 10^20 以上状态空间，适用于缓存一致性协议等大规模并发系统。

3.4.3 有界模型检查（BMC）

将性质验证转化为命题逻辑 SAT 可满足性问题，在有限步长 k 内寻找反例：

enc(M, k) ∧ enc(¬ψ, k)

若公式可满足，SAT 求解器输出一条违反性质的路径。BMC 擅长找反例，但证明“无错”需要增加 k 直至覆盖完整状态空间。

3.4.4 反例路径生成

模型检查失败时，工具自动生成一条“从初始状态到违法状态”的有限执行路径。该路径可映射回 RTL 仿真波形，快速定位缺陷根因。