越过 |-> 和 ##[m:n]：这个赛道从哪里接着讲

这个赛道不是从零开始的。SV assertions（第 15 章）已经打下了真正的基础：immediate assertion、第一对 property/sequence、|-> 蕴含操作符、##[m:n] 范围延迟，以及 assert property (...)——还带着自己的对比表和三道正好检查这些内容的测验题。在这里把这些再教一遍会浪费一整章。这一章要做的，是精确找到那套工具集恰好用尽的地方。

第 15 章已经给了你什么

用一段话讲清楚，因为它值得摆在眼前，而不是重新推导一遍：一个 immediate assertion（assert (cond) else ...;）检查的是当下这一刻，在零仿真时间内成立的条件。一个 concurrent assertion 建立在 property 之上，在时钟上采样（@(posedge clk)），能描述跨多个周期的关系——req |-> ##[1:3] ack; 的意思是"只要 req 为真，ack 就必须在接下来的 1 到 3 个周期之内变为真"。sequence 抽取一个可复用的多周期模式，供不止一个 property 引用。这就是第 15 章留给你的完整工具集。

一个那套工具集表达不出来的需求

拿第 15 章自己的例子，再加上一条要求——这是真实的握手协议经常会有的那种要求：req 必须从它变高的那一刻起持续保持高电平，直到 ack 终于到达为止——不能中途撤回又重新拉高，不能出现毛刺。只用第 15 章教过的东西试着写出来：

property req_ack_p;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty

这个 property 做不到这件事，而且值得亲眼看清楚为什么，而不是单凭猜测。|-> 在 req 某个周期为真的时候触发；紧接着的 ##[1:3] ack 问的只是 ack 会不会在接下来的 1 到 3 个周期里的某个时刻变为真。这条表达式里没有任何东西约束 req 自己在这几个周期里到底做了什么。一段本该明显违反"必须持续保持直到被应答"这条规则的轨迹，却能不出任何声地通过这个 property：

req 实际上只在一个周期里真正拉高过，紧接着下一个周期就掉下去了，一直低到两个周期之后 ack 才出现——这正是"持续保持"这条规则存在的意义所在、要禁止的那种毛刺。req_ack_p 完全没有注意到，因为它从来没有被要求在触发之后再去看一眼 req。这不是这个 property 写错了——这是对 |-> 和 ##[m:n] 单独使用时到底能说什么、不能说什么的一个如实描述。要表达"在整个窗口期间持续为真"，而不只是"窗口里某个时刻变为真"，需要一个不同的操作符：throughout，第 3 章会跟第 15 章没来得及讲的其他 sequence 操作符词汇一起讲到它。

剩下的全景图

这一个缺口是有代表性的，不是全部。以下是第 15 章留给这个赛道的其余内容，按这个赛道讲到它们的顺序排列：

• 重复操作符（[*N]、[->N]、[=N]）以及 throughout/within/first_match——第 3 章。
• |=>，非重叠蕴含（第 15 章只教过 |->），外加 disable iff 和 property 级别的 not/and/or——第 4 章。
• 针对 axil_regfile 的真实协议合规性断言，检查 dv-methodology 已经发现过、从没被测过的场景——第 5 章。
• bind，不改动 DUT 源码也能给它挂上一个检查器——第 6 章。
• 断言覆盖率（cover property），闭合回 dv-methodology 已经建好的覆盖率词汇——第 7 章。

接下来的第 2 章，讲的完全不是语法——是这一切到底值不值得学，跟自己手写一个等价检查老老实实地对比过之后再下结论。

一句关于验证可行性的话，提前说

在这个环境里直接确认过，不是假设出来的：Icarus Verilog 能正常解析 immediate assertion 和普通的过程式代码，但在最简单的 concurrent assertion（property/sequence/assert property）上会以一个硬性语法错误失败——它甚至都还没走到检查逻辑对不对的那一步。bind 也是同样的方式解析失败。这意味着从第 3 章开始，几乎每一个例子都没有本地核实的办法——跟 dv-methodology 的 Coverage 模块在 covergroup 上的处境一模一样。EDA Playground 上的一个商业级仿真器（比如这个网站一直在用的 Aldec Riviera-PRO）才是这些例子真正能跑起来的地方。第 2 章那段手写的对比代码是个例外——它是普通的过程式 SystemVerilog，Icarus 能顺利跑通。

小结

• 第 15 章已经教过 immediate assertion、property/sequence、|-> 和 ##[m:n]——这个赛道不会把这些再讲一遍。
• |-> 和 ##[m:n] 合在一起，只能检查一个结果在窗口内某个时刻有没有变为真；它们对触发信号在窗口剩下的时间里做了什么完全没有约束，这是一个真实的、可以演示出来的缺口，不是风格上的偏好。
• 这个赛道剩下的部分补上了这个缺口，还有另外五个：重复操作符、throughout/within/first_match、|=>、disable iff、bind，以及断言覆盖率。
• Concurrent assertion 和 bind 在 Icarus 里完全解析不了——这个赛道几乎全部内容都需要一个商业级仿真器才能真正跑起来。