极客工场

Appearance

共 1,618 字预计阅读约 5 分钟

SVA 断言实战：sequence/property、握手协议检查与空真断言陷阱 ​

更新时间：2026-09-14。本文是「集成电路大类 · 芯片设计 · 数字验证」实操序列第三篇。功能验证总览 里断言被定义为「在运行中检查设计应满足的条件」。这一篇把它写出来：SystemVerilog Assertion（SVA）既能在仿真里实时报错，也能在 形式验证 里作为待证明的性质。断言管「协议/时序对不对」，数据算得对不对仍交给 scoreboard。

本文要回答的问题 ​

  • 立即断言和并发断言用在什么场合？
  • property、sequence、|->、|=> 怎么念、怎么触发？
  • 怎么用一小段断言盯住 valid/ready 握手、X、FIFO 溢出？
  • 为什么断言「全绿」也可能一个都没真正检查到（空真陷阱）？

一、两类断言：立即 vs 并发 ​

立即断言（immediate assertion） 像过程语句里的 if，碰到就求值，适合组合判断：

systemverilog
always_comb begin
  assert (state != FSM_X) else $error("illegal FSM state");
end

并发断言（concurrent assertion） 基于时钟，在时钟沿采样、描述跨周期时序，是协议检查的主力，用 property + assert property：

systemverilog
// valid 一旦拉高，在握手完成前必须保持稳定（valid 不能先撤）
property p_valid_stable;
  @(posedge clk) disable iff (!rst_n)
    valid && !ready |=> valid;                       // 本拍没握手，下拍 valid 还得在
endproperty
a_valid_stable: assert property(p_valid_stable)
                  else $error("valid dropped before ready");

disable iff (!rst_n) 在复位期间关掉断言，否则复位阶段的 X 会刷一堆假错误。

二、sequence 与 property：把时序拼成句子 ​

  • sequence（序列）：描述「一个或多个周期内信号的布尔模式」。
  • property（性质）：在 sequence 上加触发关系、蕴含，成为可断言/可假设/可覆盖的命题。

最关键的两个蕴含操作符：

算子读法含义
a |-> ba 成立则当拍 b 必须成立重叠蕴含
a |=> ba 成立则下一拍 b 必须成立非重叠蕴含

常用重复/时序算子：

算子含义
##N s延迟 N 拍后看 s
s [*N]s 连续重复 N 拍
s [*1:$]s 连续重复 1 到结束（GOTO 式等待）
a throughout b在 b 整个过程中 a 必须一直成立
s1 intersect s2两序列同时结束
$rose(x)/$fell(x)/$stable(x)上升沿/下降沿/保持

「先有触发、再谈要求」用蕴含表达，这是 SVA 的思维方式：不要写成一个从头成立到尾的大表达式，而是「当某前提发生时，后续必须如何」。

三、实战：valid/ready 握手的几条铁律 ​

以标准 valid/ready（valid 表示数据有效、ready 表示能接收，二者同拍都高即握手）为例，工业级接口常检查：

systemverilog
// 1) valid 拉高后到握手前，valid 与 data 必须稳定，不能变
property p_stable;
  @(posedge clk) disable iff (!rst_n)
    valid && !ready |=> $stable(valid) && $stable(data);
endproperty
a_stable: assert property(p_stable) else $error("handshake data not stable");

// 2) data 在 valid 有效当拍不能是 X
property p_no_x;
  @(posedge clk) disable iff (!rst_n)
    valid |-> !$isunknown(data);
endproperty
a_nox: assert property(p_no_x) else $error("X on valid data");

// 3) 一旦 ready&valid 握手，FIFO 不能同时还报满（写不进去却握手）
property p_no_write_full;
  @(posedge clk) disable iff (!rst_n)
    (wr_valid && ready) |-> !full;
endproperty

其他高频检查：状态机不能出现非法编码、req 后至多 N 拍内必须见到 ack、计数器不能回绕出错、输出在 idle 时应回到默认值。这些检查贴着 DUT 接口或关键内部信号放，一旦违反当拍即报，定位比跑几万拍后在 scoreboard 发现数据错了快得多。

四、assert / assume / cover：一个性质三种用法 ​

SVA 三种动作，在仿真和形式验证中含义不同：

动作仿真中形式验证中
assert违反即报错工具要证明它恒成立或给反例
assume通常不强制当作输入约束/环境假设，限定合法激励
cover统计序列被命中检查该情形可达

同一套 property，在 testbench 里 assert 当检查器；搬到形式验证里，对输入接口用 assume（约束环境别给非法激励）、对要证的性质用 assert、用 cover 确认「某个深状态确实到得了」。这正是 SVA 能横跨仿真与形式的原因（见 形式验证入门）。

五、空真通过：断言全绿的头号骗局 ​

蕴含 a |-> b 在前提 a 从未发生时，命题在逻辑上真空成立（vacuously true）——断言一个都不报，但也一次都没真正检查过 b。典型场景：你的握手断言写得很好，可整条通路 valid 从没拉起来过，于是「全绿」。

对策：

  1. 给关键前提配 cover：cover property(@(posedge clk) valid && ready); 确认握手确实发生过若干次；
  2. 回归里同时看断言失败数和 cover 命中数，二者都要合理；
  3. 用功能覆盖率（下一篇）兜底确认协议事件真的发生。

其他常见坑：

  • 复位期不 disable：复位时信号为 X，刷假错，掩盖真问题；
  • 在 ##1 还是 |=> 上数错拍：差一拍在流水线协议里就是误报/漏报，务必画时序对；
  • 断言写成依赖内部实现：重构 RTL 后大量失效；接口级协议断言应只依赖外部契约；
  • 把数据正确性也塞进断言：复杂数据比对应在 scoreboard，断言聚焦协议与时序。

六、断言落地检查清单 ​

  • [ ] 每条并发断言都有时钟和 disable iff(rst)；
  • [ ] 用「前提 |->/|=> 结论」表达，不写全程大表达式；
  • [ ] valid/ready 稳定性、无 X、背压、溢出/下溢有覆盖；
  • [ ] 关键前提配 cover property，防 vacuous pass；
  • [ ] 报错信息带时间与信号值，能直接定位；
  • [ ] 接口断言可复用到形式验证（assert/assume/cover 分清）；
  • [ ] 协议断言与 scoreboard 数据检查分工明确。

相关与延伸 ​

断言「发生了没有」要靠覆盖率确认，见 代码覆盖率与功能覆盖率；断言在形式工具里如何被证明见 形式验证入门；承载断言、随机激励和比对的平台框架见 UVM 组件与 phase。

总结 ​

SVA 用时钟化的 sequence/property 把协议时序写成「前提蕴含结论」：立即断言管当场的组合合法性，并发断言用 |->/|=>、重复算子和 $stable/$rose 检查跨周期契约（valid/ready 稳定、valid 数据无 X、FIFO 不溢出、状态机不非法）；同一条性质在仿真里 assert 报错、在形式验证里用 assume 约束输入、用 cover 确认可达；最危险的陷阱是前提从未发生导致的 vacuous pass——所以断言必须配 cover 和功能覆盖率一起看，才能区分「真的全对」和「根本没测到」。