SVA throughout within 与 goto 重复：全程保持、区间包含与跳转匹配详解

更新时间：2026-09-28。在 SVA 断言实战 里已经见过 |->、|=> 这些骨架操作符，它们回答的是「发生了 A 之后要不要发生 B」。但真实协议里还有三类更细的需求：某个条件必须在整段传输期间一直成立（throughout）、一个短序列必须落在另一个长序列的区间之内（within）、事件之间的间隔不固定但要按顺序出现（goto repetition [->]）。这一篇专门拆这三组操作符的求值语义、波形形态和写错时的典型假象。

本文要回答的问题

• expr throughout seq 里的 expr 到底在哪些时钟沿被检查，和把条件写进 sequence 本体有什么区别？
• seq1 within seq2 的区间边界怎么算，重叠匹配时会不会漏报或多报？
• goto repetition [->n] 与连续重复 [*n]、非连续重复 [=n] 三者语义差在哪？
• 为什么 [->1] 经常和蕴含配合写出「等到某事件再检查」的断言？
• 这几组操作符在形式验证工具和仿真器里的支持度、性能开销有什么差别？

一、先把序列求值模型摆正

理解这三组操作符之前，得先回忆 SVA 序列求值的基本单位：每一个时钟沿，求值器都在问「当前这个 attempt 推进到哪一步了」。一个 sequence 是一条时间轴上的布尔条件链，匹配就是从头走到尾；fail 是中途某一步不成立。throughout、within、goto 重复都是在这条时间轴上做「区间」或「跳跃」的操作，它们不改变求值模型，只改变走的路线。

操作符	作用域	一句话语义
expr throughout seq	覆盖 seq 全程	expr 在 seq 的每一个时钟沿都为真
seq1 within seq2	嵌套区间	seq1 的匹配完整落在 seq2 的匹配区间内
b [->n]	跳转	b 非连续出现第 n 次，以第 n 次为当前点
b [=n]	计数	b 非连续出现 n 次，但当前点停在最后一次之后

表里第四行先埋下伏笔：[=] 和 [->] 的差别不在「匹不匹配」，而在「匹配结束后时间停在哪」，这一点第三节会展开。

二、throughout：让条件覆盖整个序列区间

expr throughout seq 的语义是：seq 正常匹配，同时 expr 必须在 seq 占据的每一个时钟沿（含首尾）都为真。它相当于把 expr 合取到 seq 的每一拍上，但写法上把「持续条件」和「事件骨架」分开了。

典型场景是 AXI burst 传输期间 reset_n 不得撤销、或者 awvalid 拉高到 awready 握手完成期间 awaddr 必须保持稳定：

// awvalid 拉高到 awready 拉高期间，awaddr 必须稳定
property p_addr_stable;
  @(posedge aclk) disable iff (!areset_n)
    $rose(awvalid) && !awready |->
      $stable(awaddr) throughout (awvalid [->1] ##0 awready);
endproperty

对照波形看更清楚：

这张图里 awvalid 在 t=2 拉高、awready 在 t=8 才握手。如果 awaddr 在 t=4 到 t=6 之间变了（图中从 0x1000 跳走），throughout 就会在变化的那一拍判定 fail——因为 $stable(awaddr) 在该沿不为真。注意检查点是每个时钟沿而不是「每拍结束」，毛刺在一个周期内翻两次如果恰好避开采样沿，SVA 是看不见的，这是所有采样语义的共同盲区，不是 throughout 特有的问题。

和「把条件直接写进 sequence」相比，throughout 的价值在于可读性和可维护性。下面两种写法语义等价：

// 写法 A：条件散进序列每一拍
awvalid [*1:$] ##1 (awready && $stable(awaddr));

// 写法 B：骨架是等待握手，稳定条件用 throughout 外挂
$stable(awaddr) throughout (1 [*1:$] ##1 awready);

写法 B 里骨架一眼是「等到 awready」，稳定条件是附加约束；写法 A 把两件事揉在一起，维护时改骨架容易顺手把条件弄丢。经验法则：事件流是主干，持续条件是护栏，护栏用 throughout 挂。

上图概括了求值器的行为：骨架决定时间区间，expr 被合取到区间内的每一步。expr 本身可以是任意布尔表达式（包括 $stable、$rose 这类采样函数），但不能是带时序的 sequence——seq1 throughout seq2 里左侧只允许布尔量。

三、within：判断一个序列是否被另一个序列包住

seq1 within seq2 要求：存在 seq2 的一次匹配，使得 seq1 的某次匹配的起点不早于 seq2 起点、终点不晚于 seq2 终点。一句话：seq1 完整落在 seq2 的时间窗里。它用于「在长事务窗口内必须发生某个子行为」的断言。

最经典的例子：一次读事务（从 arvalid 握手到 rlast 握手）窗口内，必须出现过至少一次 rdy && vld 的数据拍，并且整个数据阶段 rresp 保持 OKAY：

property p_data_in_read_window;
  @(posedge aclk) disable iff (!areset_n)
    (arvalid && arready) |=>
      ((rvalid && rready) [->1]) within
      (1 [*1:$] ##1 (rvalid && rready && rlast));
endproperty

在这张波形里，外层窗口从 t=2（ar 握手后的下一拍起算）延伸到 t=10（rlast 握手拍），内层序列是「第一次 r 握手」，发生在 t=6，落在 [2, 10] 内，within 成立。如果 rvalid 迟迟不来，内层 [->1] 一直匹配不到，外层窗口到 rlast 关闭时整个 within 失败——这正是我们要的：「整个读事务结束都没出过数据拍」就是个 bug 信号。

within 有三个容易踩的点：

1. 边界是闭区间。seq1 的起点可以等于 seq2 的起点，终点可以等于 seq2 终点。写「严格在内」要靠骨架里加 ##1 错开。
2. 外层必须是有限匹配。1 [*1:$] ##1 end_event 这种写法靠 end_event 关闭窗口；如果 end_event 永远不来，attempt 会无限挂着，仿真结束前不算 fail（但可以配合 strong 或在收尾检查）。
3. within 不做蕴含。它只判断「是否包住」，不判断「如果外层发生内层必须发生」。要表达「外层窗口内至少出现一次子序列」，得像上面那样把内层写成 [->1] 放在被检位置，靠 attempt 的成功与否来判定。

与 throughout 的分工可以这么记：throughout 检验的是布尔条件的持续成立（护栏），within 检验的是事件序列的嵌套关系（窗口）。一个是「每拍都成立」，一个是「区间内发生过」。

四、goto repetition [->]：跳到「下一次发生」

重复操作符一族有三个：b [*n] 是连续 n 拍，b [=n] 是非连续出现 n 次、匹配在最后一次出现后的下一个时钟沿结束，b [->n] 是非连续出现第 n 次、匹配就结束在第 n 次出现的那一拍。后两个统称非连续重复，其中 [->] 因为「跳到目标点」的行为被称为 goto repetition。

三者的差异用一条波形说：

• b [*2]：要求 t=2 和 t=4 连续两拍 b 为高——本波形不成立。
• b [=2]：t=2 第一次、t=8 第二次，匹配结束于 t=10（第二次之后的下一拍），不管 t=10 的 b 是什么。
• b [->2]：t=2 第一次、t=8 第二次，匹配结束于 t=8——当前点就停在目标事件上。

这个「停在事件上」的特性让 [->1] 成为 SVA 里最好用的「等到」原语。req |-> (gnt [->1]) ##1 check 的意思是：req 之后，时间快进到 gnt 第一次出现的那一拍，下一拍检查 check。中间隔多少拍无所谓，等不到就一直等——这正是验证握手里最常见的诉求。相比之下 [=1] 会多走一拍再交棒，后续 ##0/##1 的相位就错了，这是新手把两者混用最常见的 bug 来源。

goto 还可以带计数和范围。b [->2:4] 表示「第 2 到第 4 次出现」之间的任一次都算匹配，求值器会为每个候选终点开一条 attempt 分支。计数变大时分支数爆炸，形式验证工具里尤其明显——这条在第七节展开。

上图里求值器的行为像一个有限状态机：b 为假时空转，b 为真时计数加一，计数到 n 时把「当前时间」交给后续序列。理解了这个状态机，goto 的所有行为都是推论。

五、组合实战：三段式协议检查

真实断言往往把三者叠起来用。看一个接近项目实战的例子——校验「一次 DMA 描述符处理期间，通道 busy 必须全程为高，且窗口内必须发生一次写回（writeback）握手」：

property p_dma_desc;
  @(posedge clk) disable iff (!rst_n)
    $rose(desc_start) |->
      // 护栏：整个处理期间 busy 不掉
      (busy throughout (1 [*1:$] ##1 $rose(desc_done)))
      &&
      // 窗口：done 之前必须有过一次 wb 握手
      ((wb_valid && wb_ready) [->1] within
       (1 [*1:$] ##1 $rose(desc_done)));
endproperty

结构上是两个分支的合取：左边用 throughout 保证 busy 覆盖 [desc_start, desc_done] 全程，右边用 within 保证写回握手落在同一窗口内。拆开写两条 assertion 也完全等价，合在一条里的好处是 fail 信息集中；超过两个分支时建议拆开，coverage 统计更干净。

再给一个 goto 的典型组合——「第 4 个数据拍之后不能再有写」：

// burst 第 4 拍数据握手之后，同窗口内 wvalid 不得再拉高
property p_no_write_after_4;
  @(posedge aclk) disable iff (!areset_n)
    $rose(burst_active) |->
      not ((wvalid && wready) [->4] ##1 (wvalid && wready) [->1]);
endproperty

not 包住整个序列表达「不得出现」：先跳到第 4 次握手，再要求后面不得出现第 5 次。这类「计数到 N 后禁止」的模式在 FIFO 深度、burst 长度检查里高频出现。

六、与蕴含、abort 的交互

这三组操作符经常和 |->/|=>、disable iff 同场出现，交互顺序值得说清。

disable iff 是最高优先级的「异步复位」：任何 attempt 在任何时刻遇到 disable 条件都直接作废，throughout 覆盖的区间也不例外。所以「reset 撤销导致传输中断」不需要再用 throughout 表达——护栏只管功能条件，异常路径交给 disable iff。

蕴含与 goto 的配合有个经典陷阱：a |-> b [->1] 里，如果 b 永远不来，attempt 会悬挂到仿真结束，既不 pass 也不 fail。这在仿真里表现为 vacuous 之外的第三种沉默：不是「前提没发生所以不算」，而是「前提发生了、后果等不到」。要把它变成硬失败，得加超时：

a |-> strong(b [->1])   // 仿真收尾时未完成的 attempt 判 fail
// 或显式限时：
a |-> (b [->1] within (1 [*1:64]));   // 64 拍内必须等到

限时版本还能顺便把「等太久」这个性能问题暴露出来，比裸 strong 更有诊断价值。

within 和 overlapped 蕴含 |-> 同拍启动的问题也常见：a |-> (x within (b ##1 c))，如果 a 和 b 同拍发生，外层窗口从 b 拍起算，x 必须不早于该拍——写的人以为是「a 之后」，实际是「含 a 拍」。想错开就 |=> 或在外层骨架开头加 ##1。这类边界 off-by-one 是 SVA review 里查出率最高的缺陷类型之一。

七、工具支持与性能注意

仿真器（VCS、Xcelium、Questa）对这三组操作符支持完整，可以放心用。形式验证工具的支持面要单独确认：[->]、[=] 在有界模型检查里会被展开成状态机，计数上界大、或 [*1:$] 无界窗口长，都会让状态空间膨胀。工程对策有三条：

1. goto 计数尽量小，[->1] 和 [->2] 是甜区，[->8] 以上评估一下是否真的需要逐次计数；
2. within 外层窗口加上界，1 [*1:N] 里的 N 按协议最坏延迟取，别拍脑袋给 1024；
3. 形式环境里把这类断言单独分组，跑不动时优先裁剪带嵌套 within 的条目，保留 throughout 护栏类——后者展开开销小得多。

仿真性能方面，throughout 的开销近似于每沿多一次布尔求值，可忽略；开销大户是 [*1:$] 无界重复叠加 within，attempt 生命周期被拉长、数量随时间堆积。配合 断言覆盖率方法 的 attempt 统计直接观察活跃 attempt 数，异常增长就是收敛不了的信号。

多时钟场景下三组操作符语义仍然成立，「时钟沿」换成各自序列所在时钟域的沿即可，跨域拼接规则与 SVA 多时钟与局部变量 一致，不重复展开。

操作符	仿真支持	形式支持	开销特征
throughout	完整	完整	低，每沿一次布尔检查
within（有界窗口）	完整	多数支持	中，取决于窗口长度
within（无界窗口）	完整	谨慎	高，attempt 悬挂堆积
goto [->1..2]	完整	完整	低
goto 大计数/范围	完整	谨慎	高，分支展开

八、常见坑

• 把 [=1] 当 [->1] 用：匹配相位差一拍，后续 ##0 组合全错位，表现为断言在该过不过、波形却看不出问题。
• throughout 左侧写了 sequence：seq throughout 只接受布尔表达式，编译报语法错误都算好的，个别工具静默截断更坑。
• within 外层没有关闭事件：attempt 永远悬挂，断言从不 fail，给人「这条断言很稳」的假象。
• 用 disable iff 表达「传输期间条件成立」：那是 throughout 的活；disable iff 是异步作废，语义完全不同。
• goto 等待的事件有毛刺风险：事件表达式先加防抖（如要求连续两拍）再 [->1]，否则一次毛刺就把 attempt 放跑了。
• 边界 off-by-one：within 的闭区间、|-> 与 |=> 的同拍差异，review 时对波形数格子，别凭感觉。

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

• 向上承接：SVA 断言实战 给出蕴含、序列、## 延迟的骨架，本篇深入区间与跳转三组操作符。
• 横向相关：SVA 多时钟与局部变量 处理跨时钟域的序列拼接，与 within 的窗口语义经常同场出现。
• 落地延伸：断言绑定与覆盖率方法 讲这些 property 如何 bind 到 DUT 并统计 attempt/vacuous/cover 命中。
• 验证全景：协议总线验证手册 里有大量「传输窗口内条件保持」的真实协议断言可对照。

总结

SVA throughout within 与 goto 重复是序列操作符里的「区间三件套」：expr throughout seq 把布尔护栏钉在序列的每一个时钟沿上，seq1 within seq2 判定一个匹配完整落在另一个匹配的闭区间内，b [->n] 把时间快进到第 n 次出现的那一拍——掌握「throughout 管持续、within 管包含、[->] 管等待与定位」这条分工线，就能写出既精确又不漏检的协议时序断言。