极客工场

Appearance

共 2,630 字预计阅读约 9 分钟

FSM 状态机验证：状态覆盖、转移覆盖与非法跳转断言端到端做法 ​

更新时间：2026-09-25。有限状态机（Finite State Machine，FSM）几乎出现在每一个数字模块里：总线仲裁、UART 收发、AXI 握手、缓存控制，核心逻辑都是一张状态转移图。FSM 的 bug 有个共同特征——正常激励永远走的是主干路径，错的是那些冷门边和不该发生的跳转。这正是 代码覆盖率与功能覆盖率 里 FSM coverage 一项要专门展开讲的原因，也是本篇把 FSM 状态机验证单独打通的理由：断言怎么写、覆盖怎么收、随机怎么补，一篇讲透。

本文要回答的问题 ​

  • FSM 状态机验证里，「状态到达过」和「合法转移都走过」为什么是两件事，各怎么度量？
  • 非法跳转、未列举输入、死锁/活锁、复位行为分别用什么手段查？
  • Mealy 和 Moore 输出怎么和状态/输入核对，testplan、SVA、covergroup 怎么分工落地？

一、FSM 验证的对象：节点、边、输出三层 ​

以一个简化的总线请求状态机为例：IDLE 收到请求进 REQ，仲裁授权后进 GRANT，传数据在 BUSY，正常结束进 DONE 再回 IDLE；任何阶段出错进 ERROR，由 ERROR 回到 IDLE。下图就是验证对象——节点（状态）、有向边（合法转移）、输出，FSM 状态机验证就是逐层证明它们与规格一致。

FSM 状态机验证：状态覆盖、转移覆盖与非法跳转断言端到端做法 示意图（第 3 张）

对着图读，验证点分三层：

  • 节点层：7 个状态（含复位入口）每一个都要被到达，这叫状态覆盖（state coverage）；
  • 边层：图上每一条带条件的有向边都要真实走过，这叫转移覆盖（transition coverage）。注意「到过 BUSY」不等于走过 GRANT→BUSY，也不等于走过 BUSY→ERROR；
  • 输出层：Moore 型输出只随状态变（如 BUSY 态拉高 busy），Mealy 型输出随状态和输入共同变（如 REQ 态且 gnt=1 当拍给出响应），都要核对。

此外还有图上不该存在的东西：BUSY→IDLE 这种非法跳转、case 没列举到的输入编码、进入 ERROR 后再也不出来（活锁/死锁），这些覆盖度量不到，必须靠断言。

二、testplan：先把状态图翻译成可回溯条目 ​

写激励之前先出验证计划，每条挂回状态图的一个元素，避免「随机跑了很多但说不清测了什么」。

编号验证点类型度量/检查手段
TP1复位后一拍内进入 IDLE，输出为空闲值复位SVA 断言
TP2IDLE/REQ/GRANT/BUSY/DONE/ERROR 全部到达状态覆盖coverpoint bins
TP3图中 9 条合法边全部走过，且各 ≥N 次转移覆盖transition bins
TP4非法跳转（如 BUSY→IDLE、DONE→BUSY）永不出现非法跳转SVA 断言
TP5未列举输入/default 分支行为符合规格边界定向 + 随机非法值
TP6ERROR 必须在 M 拍内由 err_clr 清回 IDLE活性时序上界断言
TP7Moore/Mealy 输出与状态、输入一致输出核对SVA + scoreboard
TP8背靠背请求、REQ 阶段撤请求、GRANT 后延迟 start场景随机约束 + 定向

这张表也是 SVA 断言实战 里「cover property 度量发生、assert property 禁止发生」分工的实例：合法行为靠覆盖收敛，非法行为靠断言拦。

三、SVA：合法转移集合、非法跳转与输出一致 ​

最省事的合法转移写法是把「当前态→下态」限定在一个合法集合里，新增边只改一处：

systemverilog
// 合法转移对集合：复位解除后，每次跳转必须是集合中的一条边
property p_legal_transition;
  @(posedge clk) disable iff (!rst_n)
  ({state, nstate}) inside {
    {IDLE,IDLE}, {IDLE,REQ},  {REQ,GRANT},
    {GRANT,BUSY},{BUSY,DONE}, {DONE,IDLE},
    {REQ,ERROR}, {BUSY,ERROR},{ERROR,IDLE}
  };
endproperty
a_legal: assert property(p_legal_transition);

这一条同时完成两件事：任何规格外的跳转（BUSY→IDLE、DONE→BUSY、跳到 X 态）当场报错，等价于覆盖了所有非法跳转的检查，不必为每对非法状态各写一条。复位行为单独断言：

systemverilog
a_reset: assert property (@(posedge clk) !rst_n |=> state==IDLE && busy==0);

输出核对区分 Moore 与 Mealy：Moore 输出只看状态，Mealy 输出要带上输入条件。活性检查（防死锁/活锁）用有界时序，防止机器卡在某个状态永不前进：

systemverilog
// Moore：BUSY 态 busy 必须为 1
a_moore: assert property (@(posedge clk) disable iff (!rst_n)
          state==BUSY |-> busy===1'b1);

// Mealy：REQ 态当拍 gnt=1，则下一拍必须进 GRANT
a_mealy: assert property (@(posedge clk) disable iff (!rst_n)
          state==REQ && gnt |=> state==GRANT);

// 活性：进入 ERROR 后，err_clr 必须在 16 拍内出现并回到 IDLE
a_progress: assert property (@(posedge clk) disable iff (!rst_n)
          state==ERROR |-> ##[1:16] (err_clr && state==IDLE)[->1]);

##[1:16] 给恢复时间定了上界：ERROR 里无限等待的活锁、互相等待握手的死锁，都会因为「超时没回到 IDLE」而失败。

四、covergroup：枚举状态、转移对 bins 与非法桶 ​

断言保证「不坏」，覆盖率回答「合法的有没有走全」。状态用枚举后，bins 可以让工具按枚举值自动展开，不必手写每个状态；转移用 (A => B) 语法直接对应状态图上的边：

systemverilog
covergroup cg_fsm @(posedge clk);
  cp_state: coverpoint state {
    bins st[] = {IDLE, REQ, GRANT, BUSY, DONE, ERROR}; // 状态覆盖
  }
  cp_trans: coverpoint state {
    bins idle_req   = (IDLE  => REQ);
    bins req_grant  = (REQ   => GRANT);
    bins grant_busy = (GRANT => BUSY);
    bins busy_done  = (BUSY  => DONE);
    bins done_idle  = (DONE  => IDLE);
    bins to_error[] = (REQ, BUSY => ERROR);
    bins err_idle   = (ERROR => IDLE);
    option.at_least = 8;   // 每条边至少 8 次，一次偶然不算
  }
  cp_out: coverpoint {state, busy, gnt};  // 输出随状态的组合采样
endgroup

要点有三：bins st[] 的数组语法让枚举增删状态时 bins 自动跟着变；(REQ, BUSY => ERROR) 一次列全进入 ERROR 的多条边；option.at_least 把「走过」提高到「走过足够多次」。规格禁止的边还可以用 illegal_bins 再设一道功能性防线，和断言互相印证。若状态编码是向量而非枚举，bins st[] = {[0:$]} 配合工具的 FSM 提取也能自动生成节点与边，仿真器的 FSM coverage 报告与这个手写 covergroup 对照看，两边都没有空洞才算收敛。

五、激励策略：定向走查打底，随机撕边 ​

纯随机在 FSM 上效率不高：合法边大多带苛刻的输入条件（last=1、gnt=1），纯随机会反复在 IDLE 自环。实践是两段式：

  1. 定向走查打底：按状态图把每条主干边（IDLE→REQ→GRANT→BUSY→DONE→IDLE）走一遍，TP1、TP5 和复位类用例直接定向，保证基本功能与所有冷状态（ERROR）至少可达；
  2. 受约束随机撕边：随机化输入时序与异常注入——REQ 阶段随机撤请求、GRANT 后随机延迟 start、随机拍点注入 timeout/bus error、背靠背发请求。约束里用 dist 控制异常概率，异常太稀就调权重，让 ERROR 的两条进入边和恢复边快速达到 at_least。

合并覆盖率时要区分两类空洞：某条合法边反复为 0，先查是不是约束把它的触发条件封死了——比如异常注入概率设得过低，回到约束调 dist 权重比新增定向用例更值得；若某条边在规格上就不可能发生（如 GRANT 态收到 bus error 无定义），不能放着不管，要在 testplan 上写明「为何不适用」并在评审后从覆盖模型排除，留下书面记录。每个 seed 还应固定随机种子并入库，复现失败时用同一 seed 直接回放。

回归后合并覆盖率，对照第二节 testplan 逐行销项：状态 100%、合法转移 bins 全绿、断言零失败、活性检查各 seed 通过，FSM 状态机验证这一项才可以签核。

六、手段分工与四个常见坑 ​

FSM 验证的手段选择可以概括成下图：合法的、要被度量的行为交给覆盖率；非法的、禁止的行为交给断言；二者都在 testplan 上挂账。

FSM 状态机验证：状态覆盖、转移覆盖与非法跳转断言端到端做法 示意图（第 4 张）

这张图也回答了「为什么断言和覆盖不能互相替代」：转移 bins 为 0 说明合法边没走到（激励问题），断言失败说明走了规格不允许的行为（RTL 问题），信号完全不同。落地时四个坑最常见：

  • 断言 vacuous 通过：蕴含前件从没成立，断言永远「成功」却什么也没查。state==ERROR 开头的属性要配一个 cover property 确认 ERROR 确实到达过，否则活性断言是空过；
  • case 没列全又没有 default：综合出锁存，仿真里输入取未列举编码时状态保持，非法跳转断言却因为「状态没变」而放行。TP5 必须定向灌未列举编码，并确认工具的 branch coverage 里 default 出口被走过；
  • 只看工具 FSM coverage、不写功能覆盖：工具按 RTL 提取的边里包含 RTL 多写出来的错误边，走到了还给你记 100%。合法边集合要以规格为准、由人在 covergroup 和断言里各定义一遍，两份对不上就要评审；
  • 异步复位/上下电场景漏测：在 BUSY 中途拉复位最容易暴露状态没清零、输出残留。复位断言不要只在仿真开始时生效，随机测试中也应随机插入复位，确认任意状态都能回 IDLE。

这一篇在知识体系里的位置 ​

本篇是「集成电路大类 · 芯片设计 · 数字验证」序列的长尾专题。FSM 状态机验证所依赖的覆盖率签核口径见 FSM 状态机验证的覆盖率基础；FSM 状态机验证里断言、cover property 与多拍时序操作的系统写法见 FSM 状态机验证的 SVA 写法；随机异常注入的约束权重控制见 受约束随机验证 CRV。

总结 ​

FSM 状态机验证按「节点、边、输出、活性」四层展开：covergroup 用枚举 bins 收状态覆盖、用 (A => B) 转移 bins 收全部合法边并设 at_least，SVA 用合法转移对集合一次性拦住所有非法跳转，再分别断言复位进 IDLE、Moore/Mealy 输出与状态和输入一致、ERROR 在有界拍数内恢复以防死锁活锁；激励上定向走查保证主干和冷状态可达、受约束随机专撕异常边与背靠背场景，最终对照 testplan 做到状态全覆盖、合法边全绿、断言零失败才算收敛。