4. 断言中的时序与序列操作

在 SystemVerilog 断言（SVA）中，布尔表达式只能描述“某一拍是否成立”，而真实的总线协议几乎都依赖跨时钟周期的时序关系：请求拉高后若干拍内必须收到应答、应答期间数据必须保持稳定、某信号必须在整个事务期间持续有效。要表达这些关系，就必须使用序列（sequence）与时序操作符。本节围绕 ##、throughout、within、intersect 四个核心构造，完成一个总线握手协议的断言建模。

四个时序操作符的语义定位

先明确每个操作符“管什么”：

• ##n：固定延迟，表示序列起点之后第 n 拍发生后续事件；##[m:n] 表示延迟在 m 到 n 拍之间任选，##[1:$] 表示至少 1 拍、上不封顶。
• throughout：expr throughout seq 表示布尔表达式 expr 在序列 seq 的整个持续区间内每一拍都成立，用于表达“保持稳定/持续有效”。
• within：seq1 within seq2 表示 seq1 的匹配区间完全落在 seq2 的匹配区间之内，seq2 可以更长，用于表达“包含关系”。
• intersect：seq1 intersect seq2 表示两个序列的匹配区间长度完全相同且同时成立，用于表达“严格同步的并行约束”。

关键区别在于：within 允许长度不等（内层被外层包住），intersect 要求长度严格相等。这一差别决定了它们在协议建模中的不同用途。

待建模的总线握手协议

假设一个简化的同步总线，时钟为 clk，复位 rst_n 低有效。信号定义如下（示例参数，非实测）：

• req：主设备请求，高有效；
• ack：从设备应答，高有效；
• data：8 位数据总线；
• valid：数据有效标志。

协议约定：

1. req 拉高后，ack 必须在 1 到 4 拍内拉高；
2. ack 拉高期间，req 必须保持为高，不得中途撤销；
3. ack 拉高期间，data 必须保持稳定，valid 必须持续有效；
4. 一次完整握手（req 有效到 ack 有效）必须整体落在 req 的持续区间内；
5. ack 与 valid 的有效区间必须严格等长。

逐条构造断言

约束 1：应答延迟窗口。使用 ##[1:4] 表达延迟范围：

property p_ack_latency;
  @(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:4] ack;
endproperty
assert property (p_ack_latency);

这里 $rose(req) 捕获请求上升沿，|> 为重叠蕴含，##[1:4] 表示从下一拍起 1 至 4 拍内 ack 必须为高。若第 5 拍才出现 ack，断言失败。

约束 2：ack 期间 req 保持。用 throughout 表达持续有效：

property p_req_hold;
  @(posedge clk) disable iff (!rst_n)
    $rose(req) |-> req throughout (##[1:4] ack);
endproperty

含义是：从 req 上升沿开始，直到 ack 出现为止的整个区间内，req 每一拍都必须为高。若中途 req 掉低，序列提前失配，断言报错。

约束 3：数据稳定与 valid 持续。同样用 throughout，但约束对象换成 data 与 valid：

property p_data_stable;
  @(posedge clk) disable iff (!rst_n)
    $rose(ack) |-> (valid throughout ack) and
                   (data throughout ack);
endproperty

注意 throughout 左侧是布尔表达式，右侧是序列。这里 ack 本身作为单拍序列被反复匹配，实际效果是“ack 为高的每一拍，valid 与 data 都保持不变”。

约束 4：握手区间被 req 区间包含。用 within 表达包含关系：

property p_handshake_within_req;
  @(posedge clk) disable iff (!rst_n)
    (##[1:4] ack) within (req [*1:$] ##1 !req);
endproperty

外层序列 req [*1:$] ##1 !req 描述 req 从拉高到拉低的一个完整区间，内层 ##[1:4] ack 描述应答出现的位置。断言要求应答区间完全落在 req 有效区间内，不允许 ack 出现在 req 已经撤销之后。

约束 5：ack 与 valid 严格等长。用 intersect 表达长度相等：

property p_ack_valid_sync;
  @(posedge clk) disable iff (!rst_n)
    (ack [*1:$] ##1 !ack) intersect
    (valid [*1:$] ##1 !valid);
endproperty

两个序列都描述“从拉高到拉低”的区间，intersect 要求两者起止完全对齐。若 valid 比 ack 早一拍撤销，长度不等，断言失败。若改用 within，则允许 valid 区间比 ack 短，语义就不同了。

时序操作符的语义对比

下面这张图把四个操作符在时间轴上的匹配行为并列展示，帮助区分“延迟”“持续”“包含”“等长”四种关系。

建模中的常见陷阱

第一，throughout 左侧必须是布尔表达式，不能是序列。若写成 (req ##1 ack) throughout ... 会编译报错。第二，within 与 intersect 的匹配区间长度语义不同，把 intersect 误用为 within 会导致“valid 比 ack 短”这种合法场景被误报。第三，##[1:4] 的起点是序列起点之后，不是包含起点本身，写 ##[0:4] 才允许同拍。第四，[*1:$] 这类无界重复在仿真中可能造成大量线程，建议配合 disable iff 或限定上界。

完整断言模块示例

module bus_handshake_assertions (
  input logic clk, rst_n, req, ack, valid,
  input logic [7:0] data
);
  // 约束1：应答延迟窗口
  property p_ack_latency;
    @(posedge clk) disable iff (!rst_n)
      $rose(req) |-> ##[1:4] ack;
  endproperty

  // 约束2：ack 期间 req 保持
  property p_req_hold;
    @(posedge clk) disable iff (!rst_n)
      $rose(req) |-> req throughout (##[1:4] ack);
  endproperty

  // 约束3：数据稳定与 valid 持续
  property p_data_stable;
    @(posedge clk) disable iff (!rst_n)
      $rose(ack) |-> (valid throughout ack) and (data throughout ack);
  endproperty

  // 约束4：握手区间被 req 区间包含
  property p_handshake_within_req;
    @(posedge clk) disable iff (!rst_n)
      (##[1:4] ack) within (req [*1:$] ##1 !req);
  endproperty

  // 约束5：ack 与 valid 严格等长
  property p_ack_valid_sync;
    @(posedge clk) disable iff (!rst_n)
      (ack [*1:$] ##1 !ack) intersect (valid [*1:$] ##1 !valid);
  endproperty

  assert property (p_ack_latency);
  assert property (p_req_hold);
  assert property (p_data_stable);
  assert property (p_handshake_within_req);
  assert property (p_ack_valid_sync);
endmodule

这五条断言覆盖了握手协议中最典型的时序关系：延迟窗口、持续保持、区间包含、严格等长。掌握这四个操作符的语义边界，就能把大多数总线协议的时序约束转化为可仿真的 SVA 断言，为后续覆盖率驱动验证提供稳定的检查基础。