极客工场

Appearance

共 1,904 字预计阅读约 6 分钟

SVA disable iff：复位屏蔽、abort 语义与误报消除 ​

更新时间：2026-09-28。SystemVerilog 断言（SVA）：写法和常见误区 讲了断言怎么写才不多不漏；这一篇只盯一个最常见的工程痛点：复位一拍，几十条断言集体报假失败。解法就是 disable iff——但它不是「加个条件」那么简单，异步语义、abort 家族、采样点三处坑都要认清。复位的验证视角另见 复位与初始化验证：释放时序与寄存器默认值。

本文要回答的问题 ​

  • disable iff 和把复位条件写进断言前件（if (!rst_n)）有什么本质区别？
  • 正在评估中的断言线程遇到复位，是被「杀掉」还是「判定失败」？
  • abort 家族（accept_on / reject_on / sync_accept_on / sync_reject_on）各是什么语义，什么时候用？
  • 为什么有时加了 disable iff 复位期间还是会误报？

一、没有 disable iff 时会发生什么 ​

先还原事故现场。一条握手断言：

systemverilog
// 写完地址后 3 拍内必须给 bvalid
ap_bvalid: assert property (
  @(posedge clk) awvalid && awready |-> ##[1:3] bvalid
);

仿真跑到第 200 拍，awvalid && awready 成立，断言线程启动，等 bvalid。第 201 拍测试平台拉低 rst_n 做中段复位，DUT 内部状态清空，bvalid 永远不会来——第 204 拍断言超时失败。这是假失败：设计没有错，是复位合法地打断了事务。

一个中型环境里这类断言有几十上百条，一次带中段复位的回归能刷出几百个失败，把真 bug 淹死在噪声里。断言调试的第一纪律就是：复位期间的失败必须是零。disable iff 就是干这个的。

systemverilog
ap_bvalid: assert property (
  @(posedge clk) disable iff (!rst_n)
  awvalid && awready |-> ##[1:3] bvalid
);

加了一行，语义发生根本变化：只要 !rst_n 为真，所有正在进行中的该断言线程被立即丢弃（不判成功也不判失败），复位期间也不再启动新线程。注意它和写成前件条件的区别：

systemverilog
// 错误示范：这不是等效写法
ap_bad: assert property (
  @(posedge clk) rst_n && awvalid && awready |-> ##[1:3] bvalid
);

把 rst_n 并进前件，只能阻止复位期间启动新线程；已经在跑的线程（复位前启动、复位中等待 bvalid）照样走到超时失败。前件条件只在线程启动那一刻求值一次，disable iff 则是持续监测——这是两者最本质的区别，也是新人最常踩的坑。

二、disable iff 的异步语义与复位控制波形 ​

disable iff 的另一个关键特性：它的条件表达式是异步求值的，不走采样沿。断言本体在 @(posedge clk) 的采样点取值，而 disable iff 条件在仿真时间步内任何变化都会被看到（准确说在 observed region 用当前值评估）。这意味着：即使复位拉低发生在两个时钟沿之间，进行中的线程也会立刻被中止，而不是等到下一个 posedge。

SVA disable iff：复位屏蔽、abort 语义与误报消除 示意图（第 2 张）

读这张波形图抓三个时刻：20ns 线程 T1 正常启动；45ns rst_n 在两个时钟沿之间拉低，T1 不等到 50ns 的 posedge 就被当场丢弃——这就是异步语义的价值，复位沿与时钟沿的任何相位关系下行为一致；75ns 复位释放后监测恢复，90ns 启动的 T2 走到 110ns bvalid 到来，正常判成功。整条时间线上没有一个假失败。

如果 disable iff 是同步语义（等采样沿），45ns 拉低的复位要到 50ns 才生效，T1 在 50ns 沿上可能还会先做一次求值——在复位毛刺、门控时钟等场景下这一点点窗口就足以漏出误报。

三、abort 家族：四种「半成」语义 ​

disable iff 的处置方式是「丢弃」——不上报任何结果。但有些场景你不想丢弃，而是想明确判定。SystemVerilog 提供四个 abort 操作符：

操作符条件为真时对进行中线程的处置典型用途
disable iff (expr)丢弃，不判成败常规复位屏蔽，90% 的场景
accept_on (expr)立即判成功「若某事件发生则提前算过」：如收到 cancel 即算请求已合理终结
reject_on (expr)立即判失败「某事件一旦发生必是违规」：如事务进行中收到 error 注入
sync_accept_on / sync_reject_on同上，但条件在采样沿求值条件信号本身是同步采样式协议的一部分，避免异步毛刺触发

disable iff 与 sync_* 版本的求值时机差异是真实事故源。曾见过一个环境用 accept_on (!rst_n) 表达「复位来了算事务正常结束」：复位在沿间拉低时立即判成功，恰好掩盖了一个真 bug——复位前一拍协议其实已经违规，但被异步 accept 抢先「洗白」了。换成 sync_accept_on 后，条件到采样沿才生效，违规先被抓到。经验法则：屏蔽用 disable iff，裁决用 sync_accept_on / sync_reject_on，裸 accept_on / reject_on 只在确认条件是干净电平时用。

四、工程落地：一处定义，全域生效 ​

逐条断言加 disable iff 既啰嗦又容易漏。两条工程纪律：

第一，在模块级统一屏蔽。default disable iff 声明让其后所有断言自动继承复位条件：

systemverilog
module axi_checker (input logic clk, input logic rst_n, ...);
  default disable iff (!rst_n);

  ap_bvalid: assert property (@(posedge clk)
    awvalid && awready |-> ##[1:3] bvalid);
  ap_wlast:  assert property (@(posedge clk)
    wvalid && wready && wlast |-> ##1 !wvalid);
  // 后续新增断言自动带屏蔽，不怕漏
endmodule

第二，屏蔽条件用「整个复位窗口」而不只是复位引脚。很多设计复位释放后还有若干拍的初始化序列（寄存器加载、FIFO 指针归零），这期间断言同样不该启动。把 checker 的屏蔽条件定义成一个组合信号：

systemverilog
logic init_done;  // 复位释放且初始化序列完成
default disable iff (!init_done);

配合 复位与初始化验证：释放时序与寄存器默认值 里的 init_done 判定方法，屏蔽窗口与设计真实可用窗口严格对齐。剩下唯一要警惕的是屏蔽过头：若 init_done 逻辑本身有 bug 一直不拉高，所有断言静默失效，回归全绿但什么也没验。对策是加一条反向断言——assert property (@(posedge clk) !rst_n |-> ##[1:MAX] init_done)，保证屏蔽窗口有上界，checker 不会被永久麻醉。

最后提一句调试口径：加了 disable iff 后，「复位期间断言静默」是预期行为，统计覆盖率时这部分尝试（attempt）会被记为 disabled 而非 vacuous success，做断言覆盖率分析时别把两者混为一谈，详见 覆盖率模型：covergroup 与 bins 设计 对覆盖口径的讨论。

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

总结 ​

SVA disable iff 是并发断言的复位屏蔽开关：条件异步求值、持续监测，进行中的线程遇复位即被丢弃而不判失败，这是它与前件条件的本质区别；裁决类需求用 sync_accept_on / sync_reject_on，工程上用 default disable iff (!init_done) 一处定义全域生效，并补一条「屏蔽窗口有上界」的反向断言——做到这些，复位期间的假失败归零，断言也不会被静默麻醉。