极客工场

Appearance

共 2,317 字预计阅读约 8 分钟

SystemVerilog Assertion 断言模板：握手、复位、空满与独热 ​

更新时间：2026-10-31。芯片设计入门验证模板篇，属于 芯片设计入门系列。很多接口错误并不是功能完全不对，而是只在某一拍越界：反压时数据变了、复位后状态没清、空 FIFO 又弹了一次。SystemVerilog Assertion 断言模板把这些跨周期约定写成仿真器持续检查的性质，比等测试台末尾比对一个结果更早暴露问题。

首屏答案：先从五条性质起步——握手用 valid && !ready |=> valid && $stable(data)；同步复位用 !rst_n |=> 状态回到初值；空弹与满写分别要求下一拍计数不变；独热授权用 $onehot0(grant)。复制后替换信号名和复位初值即可。本文五个性质都在 Verilator 5.020 中跑过正常与故意失败路径，不把语法支持范围扩大到未经验证的 SVA 特性。

本文要回答的问题 ​

  • 四类 SystemVerilog Assertion 断言模板各自拦截什么错误？
  • |->、|=>、$stable 和 $onehot0 在这里分别表达什么？
  • 为什么 FIFO 的空满模板要排除同拍反向操作？
  • 断言报错后，应该看哪些信号定位根因？
  • 哪些模板已在真实仿真中验证，工具边界在哪里？

一、四类模板怎么选 ​

SystemVerilog Assertion（SVA，断言）是在时钟采样点检查设计约束的机制。下面的卡按接口语义分组：握手管数据保持，复位管确定初值，空满管计数边界，独热管互斥授权。它们不是互相替代的四种写法，而是可以同时挂在同一个设计上的四组检查。

四类高频断言：把接口约定变成逐拍检查

读这张图时抓住「触发条件」和「失败现象」两列：断言平时静默，不代表没有执行；只有前提成立而结果不成立时才报错。复制模板前先核对设计语义，尤其是空满边界是否允许同拍读写。

模板核心表达式失败时优先检查
握手反压后保持 valid/data上游是否撤销请求，数据寄存器是否被覆盖
复位复位后状态回初值复位极性、分支遗漏、非阻塞赋值冲突
FIFO 空满非法操作后 count 稳定指针与计数更新是否缺少边界保护
独热$onehot0(grant)多个授权分支是否同时成立

二、握手：反压期间不能换数据 ​

valid/ready 接口只有两者同拍为高才完成传输。若 valid=1 而 ready=0，上游必须继续请求，并保持负载稳定，否则下游可能采到一笔从未完整存在的数据。

systemverilog
a_handshake_stable: assert property (
    @(posedge clk) disable iff (!rst_n)
    valid && !ready |=> valid && $stable(data)
);

|=> 是非重叠蕴含：本拍看到反压，检查下一拍。$stable(data) 比较相邻采样值，disable iff (!rst_n) 则让复位期间不检查该性质。失败时先看 valid 是否被上游提前拉低，再看 data 是否在等待期间被新请求覆盖。若协议允许等待中撤销 valid，这条模板就不适用，不能为了消报错直接删掉保持要求。

三、复位：检查初值，不只检查复位线 ​

拉低复位线只是输入动作，真正需要保证的是状态结果。下面的模板适用于同步复位：state 和 count 在复位后的下一拍应分别为 IDLE 与 0。

systemverilog
a_reset_state: assert property (
    @(posedge clk) !rst_n |=>
    (state == IDLE && count == 3'd0)
);

这里没有 disable iff，因为复位正是被检查对象。若断言失败，而波形里的 rst_n 确实为低，常见根因是某个寄存器漏写复位分支、多个时序块驱动同一寄存器，或设计实际采用异步复位却套用了同步模板。替换初值时要覆盖所有影响后续控制的关键状态，不要只检查一个容易通过的 state。

四、FIFO 空满：非法操作不得推动计数 ​

空满断言适合放在计数式同步 FIFO 上。empty 时禁止只弹不写，full 时禁止只写不弹；即使上层误发请求，下一拍的 count 和边界状态也应保持不变。

systemverilog
a_fifo_underflow: assert property (
    @(posedge clk) disable iff (!rst_n)
    empty && pop && !push |=> empty && $stable(count)
);

a_fifo_overflow: assert property (
    @(posedge clk) disable iff (!rst_n)
    full && push && !pop |=> full && $stable(count)
);

两个 !push、!pop 不是装饰：满时同拍读写通常合法，空时同拍读写是否直通则取决于协议，不能用简单的「计数不变」一概而论。失败时先确认越界请求那一拍，再检查计数器的加减使能是否分别受 !full、!empty 限制。FIFO 的基本结构可对照 FIFO 与仲裁器基础。

五、独热：允许多个请求，不允许多个授权 ​

优先级仲裁器可以同时收到多个 req，但同一拍只能给一个 grant。$onehot0 允许全零或只有一个 1，正好覆盖「无请求时无授权」的空闲态。

systemverilog
a_grant_onehot0: assert property (
    @(posedge clk) disable iff (!rst_n)
    $onehot0(grant)
);

这条性质没有前件，每个非复位采样沿都检查。若协议要求任何工作拍都必须授权，应改用 $onehot；若 grant 是独热码但多位宽未知值也需要拦截，还应另加未知值检查。多热报错通常意味着多个 if 分支同时置位，或组合逻辑缺少默认赋值，排查时把 req 与各分支条件放在同一拍对照。

六、真实运行：正常路径与故意失败都要过 ​

测试台把五条性质挂在一个最小模型上，第一轮正常激励，第二轮分别注入反压改数、复位漏清、满写、空弹和多热授权。注入逻辑只服务测试，不属于设计模板。

Verilator 实测：五个性质正常全过，注错后各捕获一次

正常轮的 failures=0 表示五次性质检查没有误报；注错轮每出现一条 EXPECTED_FAIL，都是对应断言的动作块真实执行。最终 failures=5 说明五个性质没有「写了却永远不触发」的空检查。

exp-log
=== injected-fault run: every property must report its violation ===
EXPECTED_FAIL handshake: valid/data changed while stalled
EXPECTED_FAIL reset: state/count did not return to reset values
EXPECTED_FAIL fifo-full: full push changed count
EXPECTED_FAIL fifo-empty: empty pop changed count
EXPECTED_FAIL onehot: multiple grant bits are high
RESULT PASS: 5/5 deliberate violations detected; failures=5
- tb_sva_templates.sv:231: Verilog $finish

本版只使用 Verilator 5.020 已实际支持的并发断言子集：时钟采样、disable iff、简单布尔表达式、非重叠蕴含以及 $stable/$onehot0。复杂序列、局部变量和多拍范围不在本文模板内；也不要据此推断其他仿真器支持同样语法。

七、放进真实工程前的三个改写点 ​

把检查放在设计边界附近。 断言引用的应是模块端口或语义稳定的内部状态，不要依附随时会重构的中间组合信号。例如 FIFO 模板检查 count 很直观；若真实设计只有读写指针而没有计数器，就应改写为指针差值或边界标志，而不是为了套模板额外引入一份冗余计数。

区分「没报错」与「前提没发生」。 蕴含表达式的前件不成立时，该次检查会自然通过。若整个测试从未制造反压，握手断言即使始终静默，也不能证明保持逻辑正确。因此回归激励必须真的走到反压、复位、空弹、满写和多请求场景；本文的注错轮正是用来确认失败路径可观测。

让报错文本直接服务定位。 默认断言错误通常含时间、层次和性质名，工程里还可以在动作块补充 valid、ready、count 或 grant 的采样值。不要只写一句笼统的协议错误，也不要把所有失败都映射成同一个消息。断言名称保持唯一，看到日志后才能从失败性质回到对应接口约定。

实验环境 ​

  • 机器/系统：本机 macOS + geek-eda:0.2 Docker 镜像
  • 工具版本：Verilator 5.020 2024-01-01 rev（Debian 5.020-1）
  • 日期：2026-10-31
  • 完整命令：verilator --binary --assert --timing -Wall -Wno-fatal --top-module tb_sva_templates tb_sva_templates.sv，随后运行 ./obj_dir/Vtb_sva_templates 与 ./obj_dir/Vtb_sva_templates +INJECT_FAULTS

代码获取 ​

完整测试台和运行脚本在公开仓 https://github.com/derekzhuo/geek-doc.cn/tree/main/experiments/tpl-sva-assertions。进入目录后执行 bash run.sh，即可复现正常与注错两轮结果。

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

本篇与 两级同步寄存器 Verilog 模板 都属于「可直接复制并跑通」的入门件：前者检查接口与状态约束，后者处理单比特跨时钟域同步。FIFO 信号语义与仲裁场景分别见 FIFO 与仲裁器基础 和 芯片设计入门系列。

总结 ​

SystemVerilog Assertion 断言模板的价值，是把握手保持、复位初值、FIFO 空满和独热互斥从口头约定变成逐拍检查。复制时保留触发条件与采样语义，按设计替换信号和初值，不要用删断言来消错。Verilator 5.020 实测中，五个性质在正常激励下零失败，在五类故意违例下各触发一次，模板及其失败诊断路径均已跑通。