SVA 重复算子：[*n]、[*m:n]、[->n]、[=n] 四种重复与延迟窗口写法全解

更新时间：2026-09-28。在 SVA 断言实践 里，property 的骨架是「前件 implication + 后件 sequence」，而 sequence 的表达力几乎全押在延迟与重复上：一笔 burst 传 8 拍、一次握手在若干拍内完成、一个事件在窗口内发生若干次——这些都靠重复算子写出来。SVA 重复算子一共四种面孔，语义差别很细，写错一个往往不是断言报错，而是断言永远假性通过。这一篇把四种算子逐一拆开，配上时序解读和协议实例。

本文要回答的问题

• [*n]、[*m:n]、[*0:$] 这些连续重复到底在什么时刻判定匹配？
• [->n]（goto 重复）和 [=n]（非连续重复）都说「发生 n 次」，差别在哪里？
• 重复算子和 ## 延迟怎么组合出「3 到 5 拍之内 ack 拉高」这种窗口语义？
• req/ack 握手、burst 传输、超时检查各应该用哪种算子，为什么？
• 空匹配（零次重复）会让断言在什么情况下悄悄通过？

一、为什么 sequence 需要重复算子

没有重复算子时，描述「valid 保持 8 拍」只能写成 valid ##1 valid ##1 valid ... 连写八遍。burst 长度是参数时，连写根本不可行。更麻烦的是不确定性：「ack 在 1 到 4 拍之内拉高」要求长度可变，「grant 到来之前 req 一直举着」要求次数未知。这两类需求正是 SVA 重复算子的分工：

• 连续重复 [*n]：布尔表达式在连续的 n 拍里每拍都为真。
• 连续重复窗口 [*m:n]：连续为真的拍数落在 m 到 n 之间，任一长度都算匹配。
• goto 重复 [->n]：表达式不必连续为真，但第 n 次为真的那一拍就是整个序列的匹配点，中间拍无所谓。
• 非连续重复 [=n]：同样数第 n 次为真，但匹配点可以延后——第 n 次为真之后允许再拖若干拍才结束。

四者的共同点是：重复的对象是一个布尔表达式（也可以是整个子序列），计数单位是采样时刻（一般是时钟沿）。[->n] 和 [=n] 的表达式只在「为真的拍」上计数，为假的拍被跳过，这是它们与 [*n] 的本质分野。

上图先把家族关系立住：三种算子都是对同一个布尔表达式的计数方式，[*n] 最严格（逐拍连续），[->n] 与 [=n] 放松了连续性，只在匹配点的定义上有所区别。后面三节逐个展开。

二、连续重复 [*n] 与窗口 [*m:n]：逐拍判定

b[*n] 的语义一句话：从当前拍开始，b 在接下来的 n 拍里每一拍都为真，且这 n 拍是背靠背连续的。任何一拍 b 掉了，整个序列这次匹配尝试就失败。注意 SVA 的序列匹配是「尝试-失败-再尝试」的：每个时钟沿都会以该沿为起点发起一次新的匹配尝试，某次尝试失败不影响其他起点。

b[*m:n] 把固定次数放宽成一个闭区间：连续为真的拍数达到 m 到 n 之间的任何一个值都构成一次匹配。这意味着它对同一起点可能产生多个匹配点（长度 m、m+1、……、n 各算一次），在 implication 前件里表现为「任一匹配都会触发后件」。[*0:$] 是特殊值：0 到无穷，即「任意长（含零次）」。

零次重复（empty match）是最容易被忽视的坑：b[*0] ##1 c 直接退化成 ##1 c，b 根本没被检查。写出 req |-> ack[*1:4] ##1 done 这种式子时，如果本意是「ack 至少举一拍再 done」，用 [*1:4] 没问题；但手滑写成 [*0:4]，done 紧跟 req 下一拍拉高也算过，ack 全程没来照样通过——断言永远不报错的假性通过就是这么来的。

这张波形图对照读：b[*3] 从第 1 拍起尝试匹配，b 在第 1、2、3 拍连续为高，第 3 拍即为匹配点（match_a 在第 2 拍处示意第 2 次尝试以长度不同失败，第 1 拍起点的尝试成功）。而 b[*4] 以第 1 拍为起点的尝试在第 4 拍失败——b 已经掉了。窗口形式 b[*2:4] 则会在第 2、3 拍各产生一次匹配。

与 ## 组合时，连续重复天然适合表达「某信号要保持 N 拍」：AXI 里 wvalid && !wready |-> wvalid[*1:$] ##0 wready 的骨架（更严谨的写法用 s_stable 或 [*1:$] 加交叠），描述「valid 举起后在 ready 到来前不得撤下」。

还有一个行为层面的细节值得记住：窗口形式的多匹配点意味着断言可能被触发多次。b[*2:4] 以同一拍为起点最多产生三次匹配，在 implication 前件里只算「有一次匹配即触发」，但在裸 assert property (b[*2:4]) 或 cover property 里，每次匹配都是独立事件。写覆盖率时用窗口算子能看到分布，写约束性断言时则要想清楚是否真的想允许长度取遍整个区间——很多「3 到 5 拍」的窗口，协议原文其实是「恰好 4 拍，但允许前后各漂一拍」，这两句在仿真里不等价，前者放过的毛刺后者会拦下来。

三、goto 重复 [->n]：跳到第 n 次为真的那一拍

b[->n] 读作「goto n」：从当前拍向后找，第 n 次 b 为真的那一拍，就是整个序列的匹配点。中间 b 为假的拍全部被跳过，不计长度。n=1 时 b[->1] 就是「等到 b 第一次为真」，是四种算子里使用频率最高的一种形态。

它解决的核心问题是「等待一个不知何时到来的事件」。req |-> gnt[->1] 表示「req 之后，gnt 至少来一次，中间的等待拍数不限」——相比 ##[1:$] gnt，goto 写法意图更清晰，仿真器内部的匹配实现也完全等价。要表达「gnt 来两次」就是 gnt[->2]：第一次为真不算结束，跳到第二次为真的那一拍才匹配。

对照波形读：req |-> gnt[->2] 从第 1 拍出发，第 4 拍是 gnt 第一次为真（计数 1，不结束），第 6 拍是第二次为真——匹配点落在第 6 拍。中间第 2、3、5 拍 gnt 为低，全部被跳过。如果这条序列后面还接 ##1 done，那么 done 检查的就是第 7 拍。

goto 重复最常见的工程形态是「恰好 n 次」配合 !b 收尾：req |-> gnt[->2] ##1 !gnt[*2] 表示 gnt 恰好来两次脉冲、之后两拍内不再来。写协议断言时「burst 内 data_beat 恰好 8 次」就是 data_beat[->8] ##1 burst_end 这类骨架。

调试 goto 序列时有个实用技巧：把布尔表达式本身做成 cover。gnt[->3] 总是不命中时，先 cover property (gnt[->1]) 确认第一次为真是否真的出现过，再逐步加次数，比直接盯着整条长序列的失败报告猜原因快得多。匹配尝试挂起（事件始终不来）在仿真报告里通常表现为「未完成的尝试」而不是失败，很多仿真器在 $assertcontrol 或结束时统计里会单独列出 offpending 数量，回归收尾时这个计数非零往往比 fail 更值得追查——它意味着断言从没真正走完过，等同于没测。

四、非连续重复 [=n]：数够 n 次，但允许拖拍

b[=n] 与 [->n] 共享「跳过为假的拍、数到第 n 次」的计数逻辑，唯一差别在匹配点的定义：[->n] 的匹配点钉死在第 n 次为真的那一拍，[=n] 在第 n 次为真之后还允许任意多拍（包括 b 再为真）才结束整个序列。换句话说 [=n] 自带的尾巴相当于 [->n] ##0 !b[*0:$]——数够 n 次之后，b 再也不为真的那些拍都算在匹配里。

这个差别什么时候要紧？看接续关系。序列 b[=3] ##1 c：第 3 次 b 为真之后，允许隔几拍，c 在某拍为真即匹配；而 b[->3] ##1 c 要求 c 必须紧跟第 3 次 b 的下一拍。典型场景是「整个 burst 里 err 标志出现 3 次，之后 1 拍内状态寄存器被读走」：err 第 3 次为真后软件未必立刻响应，用 [=3] 才符合协议意图；用 [->3] 会把合法行为误判为违规。

反过来，经验法则是：默认用 [->n]，只在「第 n 次之后确有协议允许的拖拍」时才用 [=n]。因为 [=n] 的宽松尾巴会扩大匹配空间，既拖慢仿真，也容易把本该收敛的检查放得过头。很多团队代码评审时见到 [=n] 会要求作者在注释里说明拖拍的协议依据，就是这个原因。

五、延迟窗口 ##[m:n] 与四种算子的组合

重复算子管「一个表达式出现多少次」，##[m:n] 管「两段之间隔几拍」。两者叠加才覆盖真实协议的时序描述。最常见的组合是「事件在窗口内到来」：req |-> ##[1:4] ack，表示 ack 在 req 之后第 1 到第 4 拍之间的某一拍拉高。这个窗口本身可以用 goto 加连续重复展开——##[1:4] ack 与 (!ack)[*0:3] ##1 ack 等价——但窗口写法紧凑得多，也是评审时的首选形式。

几种高频组合的对照表：

协议意图	推荐写法	语义要点
valid 保持直到 ready	valid[*1:$] ##0 ready 或 s_until_with	连续重复尾部交叠 ready
ack 在 3 到 5 拍内来	##[3:5] ack	延迟窗口，下界防 0 拍空转
gnt 恰好两次脉冲	gnt[->2] ##1 !gnt[*2]	goto 计数 + 连续否定收尾
burst 8 拍数据	beat[->8] 或 vld[*8]	取决于 beat 是否逐拍连续
事件之后允许响应延迟	evt[=3] ##[1:8] resp	非连续重复 + 响应窗口
永不发生	!b[*1:$]（在 always 块里）	连续重复配合隐式时钟

写窗口时还有一个方向性的坑：[*m:n] 的重复对象在「为真的拍数」上取区间，##[m:n] 在「间隔拍数」上取区间，两者的下界语义不同。##[0:3] ack 允许 ack 同拍到来（配合 |-> 时即下一拍起算），而 ack[*0:3] 允许 ack 一次都不来。把「ack 至少一拍」写成 ack[*0:3] 又是空匹配陷阱的翻版。

对照波形：req |-> ##[1:4] ack 在第 3 拍即匹配（ack 第一次为高落在窗口内）；而 req |-> ack[->2] 的匹配点在第 5 拍。两个式子都「合法」，检查的却是完全不同的协议性质——前者是响应时限，后者是响应次数。写断言前先问自己「我在意的是它什么时候来，还是它来几次」，算子选型就清楚了。

多时钟场景下，每个采样沿的归属由 sequence 上的时钟决定，跨时钟写重复算子要格外小心计数基准，可结合 SVA 多时钟与局部变量 里的时钟切换规则一起读。

六、协议实例：req/ack 握手与 burst 传输

把四种算子放进两条真实协议性质的断言里收个尾。第一条是带超时的握手：req 拉高后 ack 必须在 10 拍内到来，且 ack 期间 req 不许撤。

property p_req_ack_timeout;
  @(posedge clk) disable iff (!rst_n)
    $rose(req) |-> (req && !ack)[*0:9] ##1 ack;
endproperty
a_req_ack: assert property (p_req_ack_timeout)
  else $error("ack timeout or req dropped early");

这里 (req && !ack)[*0:9] ##1 ack 是连续重复窗口的标准用法：等待期间每拍都要求 req 保持且 ack 没来，等待长度 0 到 9 拍，第 10 拍之内 ack 必须出现。它同时编码了三条性质——超时上界、req 保持、ack 至少来一次，这也是连续窗口比 ##[1:10] ack 更强的地方：后者不检查等待期间 req 是否被撤下。

第二条是定长 burst：burst_start 之后数据拍恰好 8 次，随后 burst_end 拉高。

property p_burst_len8;
  @(posedge clk) disable iff (!rst_n)
    $rose(burst_start) |-> data_vld[->8] ##1 burst_end;
endproperty
a_burst_len: assert property (p_burst_len8)
  else $error("burst length != 8 beats");

data_vld[->8] 容忍数据拍之间插入等待周期（valid 被反压拉低是合法的），只数够 8 次；若协议规定数据必须背靠背，就改写成 data_vld[*8]。一字之差对应两种协议定义，写之前对照总线手册确认 burst 是否允许 wait state——AHB 的 HREADY 拉低插入等待是合法的，用 [->8]；某些内部流式接口要求气泡为零，用 [*8]。

两条断言配合 cover property 使用还能看到匹配点的分布：握手用例里 ack 落在第 1 拍和第 9 拍的覆盖率差异，直接暴露激励是否打到了超时边界。覆盖率挂接的方法见 SVA bind 与覆盖率方法。

七、常见坑

• 空匹配放行：下界写 0（[*0:4]、##[0:3]）时表达式一次都不用为真，断言照样过。凡下界写 0 都多问自己一遍「零次是否真合法」。
• [=n] 当 [->n] 用：非连续重复的拖拍尾巴会放宽匹配空间，既慢又松；没有明确协议依据就用 goto 形式。
• 连续重复套在可能被打断的信号上：AXI valid 被反压时是合法的「保持」，但数据拍之间插气泡时 [*n] 会直接失败；先确认协议允不允许 wait state。
• 重复对象写复杂表达式却不加括号：a && b[*3] 解析为 a && (b[*3])，想要的是 (a && b)[*3]，括号省不得。
• 在带 disable iff 的 property 里数复位期次数：复位释放沿与第一次重复计数重叠时，$rose/$fell 与重复算子的交互容易漏一拍，关键计数断言建议在复位稳定后的门控信号上重新触发。
• 把 goto 当超时：gnt[->1] 是「等到它来」，永远不来则该次匹配尝试挂起不失败，断言不报错。超时检查必须用上界窗口或 s_eventually 加定时约束。
• 多时钟下默认计数基准：sequence 里显式标注 @(posedge clk) 的段落决定计数沿，漏标时钟时默认继承 property 时钟，跨时钟域断言的拍数口径很容易因此对不上设计意图。

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

• 向上承接：SVA 断言实践 给出 property/assert/assume 的整体骨架，本篇专攻 sequence 内部的重复与延迟表达。
• 横向相关：SVA 多时钟与局部变量 讲跨时钟采样与变量保存，重复算子的计数基准在那里继续展开。
• 验证环境侧：UVM 组件与 phase 里 scoreboard 的事务级检查与本文的信号级时序断言互补，一个看数据对不对，一个看时序合不合规。
• 形式验证延伸：带窗口与重复的性质是形式工具最擅长穷举的那类，接法见 形式验证入门。

总结

SVA 重复算子四种形态各管一件事：[*n]/[*m:n] 数连续为真的拍数（下界写 0 要防空匹配），[->n] 跳到第 n 次为真的那一拍（等待未知延迟事件的首选），[=n] 数够 n 次还允许拖拍（仅在协议明确允许时用）；与 ##[m:n] 延迟窗口组合后，响应时限、保持关系、burst 计数这三类最常见的协议性质就都有了标准写法。