模型检测入门：模型检测的基本概念、状态空间与状态转移系统

好，咱们今天聊聊模型检测。说实话，我刚入行那会儿，听到「模型检测」这四个字，第一反应是——这玩意儿是不是跟仿真差不多？后来踩了坑才明白，它俩完全是两码事。

模型检测，说白了就是一种自动化的验证方法。你给它一个系统模型，再给它一条性质（比如「信号A永远不能为X」），它就能告诉你：这个性质到底成不成立。如果成立，皆大欢喜；如果不成立，它还会给你一个反例——也就是一条能复现错误的路径。

我个人觉得，模型检测最迷人的地方在于：它不需要你写测试用例。你想想看，仿真你得绞尽脑汁构造激励，还得担心覆盖率够不够。模型检测呢？它自己把整个状态空间翻个底朝天，一个不漏。

状态空间：系统的「所有可能瞬间」

什么是状态空间？我习惯这么理解：一个系统在任意时刻，所有寄存器和输入信号的值，拼在一起就是一个「状态」。而所有可能的状态，就构成了状态空间。

举个例子，一个简单的计数器，只有 2 位宽。那它的状态空间有多大？

  • 00
  • 01
  • 10
  • 11

就 4 个状态。但如果你有 100 个寄存器，每个寄存器 1 位，那状态空间就是 2^100。这个数字有多大？我告诉你，比宇宙中的原子数还多。嗯，这里要注意——状态爆炸，就是模型检测最大的敌人。

核心要点：状态空间的大小 = 2^(寄存器位数 + 输入信号位数)。每增加一个寄存器，状态空间翻一倍。

我在项目中遇到过这样一个场景：一个简单的 AXI 总线仲裁器，只有 8 个 master，每个 master 只有 2 位状态。我一开始觉得状态空间不大，结果一跑模型检测，直接爆内存。后来不得不做抽象，把一些无关信号剪掉，才跑通。

状态转移系统：状态之间怎么跳

光有状态还不够，你得知道状态之间怎么跳。这就是状态转移系统要干的事。

状态转移系统，通常用一个有向图来表示。每个节点是一个状态，每条边是一个转移。转移的条件，就是组合逻辑和时序逻辑共同决定的。

举个例子，一个简单的有限状态机：

// 一个简单的 2 状态 FSM
// 状态：IDLE, ACTIVE
// 输入：start, done

always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n)
    state <= IDLE;
  else
    case (state)
      IDLE:   if (start) state <= ACTIVE;
      ACTIVE: if (done)  state <= IDLE;
    endcase
end

这个 FSM 的状态转移图就是：

  • IDLE → (start=1) → ACTIVE
  • ACTIVE → (done=1) → IDLE
  • IDLE → (start=0) → IDLE（自环）
  • ACTIVE → (done=0) → ACTIVE（自环）

你看，状态转移系统其实不复杂。但一旦系统规模上去，这个图就会变得极其庞大。我曾经调试过一个 DMA 控制器，状态转移图画出来，打印到 A0 纸上都看不清。

我的小技巧：写 RTL 的时候，尽量把状态机写成「一段式」或者「两段式」，不要用「三段式」。三段式虽然仿真效率高，但模型检测时状态转移关系反而不好提取。我吃过这个亏。

模型检测到底怎么「检测」？

模型检测的核心算法，说白了就是「穷举搜索」。它会从初始状态出发，沿着状态转移系统，把所有可达的状态都走一遍。每到一个状态，就检查一下你要验证的性质是否成立。

性质通常用 CTL（计算树逻辑）或 LTL（线性时序逻辑）来描述。比如：

  • AG (req → AF ack)：任何时候，只要 req 为真，那么最终 ack 一定会为真。
  • EF (error)：存在一条路径，最终 error 信号会为真。
  • G (ready → X busy)：全局来看，如果 ready 为真，那么下一个周期 busy 一定为真。

这些逻辑公式，模型检测工具会逐条检查。如果发现某个状态违反了性质，它就会回溯出一条路径，作为反例输出。

注意：模型检测只能验证「有限状态」的系统。如果你的系统有无限状态（比如带 FIFO 深度无限），那模型检测就无能为力了。这时候得用符号模型检测或者抽象技术。

状态爆炸：怎么破？

状态爆炸是模型检测绕不开的坎。我刚开始做形式化验证时，经常遇到「out of memory」的错误。后来总结了几条经验：

  1. 做抽象：把无关的信号剪掉。比如验证一个 FIFO 的满空逻辑，你不需要关心数据通路的具体值，只需要关心读写指针。
  2. 用 BDD：二元决策图可以把状态空间压缩成一种紧凑的数据结构。很多工具（比如 NuSMV）底层就是基于 BDD 的。
  3. 分而治之：把一个大系统拆成几个小模块，分别验证。我习惯先验证控制通路，再验证数据通路。
  4. 用 bounded model checking：只检查有限步数内的性质。虽然不保证完全正确，但工程上够用。

我曾经遇到一个项目，一个 32 位的加法器，状态空间 2^64，直接跑模型检测根本不可能。后来我把输入约束到几个典型值，再配合 bounded model checking，才把问题搞定。

一个简单的模型检测例子

咱们用 NuSMV 写一个最简单的模型检测例子。假设有一个 2 位计数器，从 0 计数到 3，然后回 0。我们要验证：计数器永远不会超过 3。

MODULE main
VAR
  count : 0..3;

ASSIGN
  init(count) := 0;
  next(count) := (count + 1) mod 4;

-- 性质：计数器永远不会超过 3
SPEC AG (count <= 3)

这个性质显然是成立的。但如果你把计数器改成 4 位，但只用了 3 位，那性质就可能不成立。模型检测会告诉你：在第 8 个周期，count 变成了 8，违反了性质。

你看，这就是模型检测的威力——它不需要你手动构造测试用例，自己就能找到边界情况。

小结

模型检测入门，其实就三件事：

  • 理解状态空间是什么
  • 理解状态转移系统怎么描述
  • 理解模型检测怎么穷举搜索

剩下的，就是多练。我建议你找一个简单的 RTL 模块，比如一个 SPI 控制器或者 I2C 控制器，试着用 NuSMV 或者 SymbiYosys 跑一下模型检测。第一次跑通的时候，那种成就感，不亚于仿真覆盖率到 100%。

嗯，今天就聊到这儿。下一章咱们聊聊时序逻辑的性质怎么写，以及怎么用 CTL 描述复杂的验证目标。

← 上一章 📖 返回目录 下一章 →