3. 模型检查（Model Checking）核心原理：状态空间搜索、时序属性、Kripke结构、不动点计算与CTL/LTL基础
问题背景：为什么需要模型检查？
在形式化验证的工程实践中，仿真（Simulation）只能证明“测试过的路径存在”，无法证明“未测试的路径不存在”。对于复杂的硬件控制逻辑、总线协议或流水线设计，状态空间可能达到 \(10^{20}\) 以上，依靠手工编写测试用例或随机仿真，覆盖率难以收敛。
模型检查（Model Checking）提供了一种穷尽式自动验证方法：它遍历系统所有可达状态，检查是否满足给定的时序属性。如果属性不成立，则自动生成一条反例路径（Counterexample），帮助工程师快速定位设计缺陷。
核心概念：模型检查的四大支柱
| 概念 | 说明 | 在Questa Formal中的角色 |
|---|---|---|
| 状态空间 | 系统所有可能的状态及状态转移关系的集合 | 由 RTL 设计自动提取，可做抽象或约简 |
| Kripke 结构 | 形式化模型 \(M=(S, S_0, R, L)\)，S 为状态集合，R 为转移关系，L 为原子命题标记函数 | 验证引擎内部表示，用于遍历和推理 |
| 时序属性 | 描述系统随时间变化的期望行为，如“请求后必然响应” | 使用 SVA/PSL 编写，或使用 CTL/LTL 描述 |
| 不动点计算 | 通过迭代计算状态集合的最小/最大不动点，判定属性是否成立 | BDD 或 SAT/SMT 引擎的基础算法 |
原理机制：Kripke 结构与状态空间搜索
模型检查的第一步是将设计转换为 Kripke 结构。每个状态包含所有寄存器、存储器和关键信号的值；状态转移对应一个时钟周期或输入激励。属性 \(\varphi\) 的验证就转化为：是否存在一条从初始状态出发的路径，使得 \(\varphi\) 在指定时刻成立或不成立。
CTL（ Computation Tree Logic）和 LTL（Linear Temporal Logic）是两种常用的属性描述语言。CTL 以状态量词和路径量词组合表达，例如 \(AG( req \rightarrow AF\ ack )\) 表示“在所有可达状态中，请求之后所有路径最终都能收到应答”。LTL 则以线性路径为语义，使用 \(\square\)（ always）、\(\Diamond\)（ eventually）、\(\mathsf{U}\)（ until）等算子描述系统所有执行路径上的时序行为。
流程步骤：一次完整的模型检查任务
- 建立模型：将 RTL 或抽象模型转换为 Kripke 结构。
- 编写属性：使用 SystemVerilog Assertions（SVA）、PSL 或 CTL/LTL 形式化描述设计意图。
- 选择引擎：根据属性类型和设计规模选择 BDD、SAT 或基于 ABC 的引擎。
- 执行验证：工具自动遍历状态空间，计算不动点。
- 分析结果：若属性失败，查看反例波形定位 bug；若成功，确认完备性和覆盖度。
案例说明：仲裁器验证
假设一个简单总线仲裁器，保证“一旦某个 master 发出请求，最终会获得 grant”。其 SVA 属性可写为：
property req_granted;
@(posedge clk)
request |=> eventually grant;
endproperty
assert property (req_granted);
Questa Formal 在验证该属性时，会从初始状态出发，遍历所有可能的状态组合。如果存在某个状态之后 grant 一直为 0，工具会返回一条反例路径，帮助工程师判断是协议漏洞还是约束缺失。
表格总结：CTL 与 LTL 核心算子对比
| 逻辑 | 核心算子 | 语义特征 | 典型场景 |
|---|---|---|---|
| LTL | \(\square\)、\(\Diamond\)、\(\mathsf{U}\)、\(\bigcirc\)（next） | 所有线性路径上的事件顺序 | 协议时序、流水线推进、信号握手 |
| CTL | \(A\)、\(E\)、\(G\)、\(F\)、\(X\)、\(U\) | 状态与路径量词组合，可表达可能性 | 复位释放、互斥访问、活锁检测 |
| CTL* | 上述全部 | 更广泛地混合路径与状态量化 | 复杂嵌套时序属性 |
误区提醒
- 把模型检查当仿真用：模型检查面向穷尽证明，不适合大数据流计算；仿真适合功能调试。
- 忽略属性正确性：属性写错，结论全错。务必先进行“正反断言”检查，故意注入错误验证属性敏感性。
- 以为状态空间总能完全遍历：实际工程中常常需要抽象、约简或假设-保证推理，否则会超时或内存溢出。
- 混淆 LTL 与 CTL 语义：LTL 的“最终”是路径上的，而 CTL 的 \(EF\) 是“存在路径可达”；换用符号时务必明确语义。
实践清单：入门模型检查应完成的 6 件事
- 用 Questa Formal 打开一个简单设计（如 Arbiter、FIFO）。
- 为设计的关键协议编写 3～5 条 SVA 断言。
- 使用 check 命令运行形式化分析。
- 故意修改设计制造 bug，观察反例波形。
- 识别模型的初始状态与 reset 约束，避免非法状态干扰。
- 记录验证时间和状态空间大小，作为后续复杂设计的对比基线。