📚 课程目录第4章 SVA断言基础与复杂控制逻辑表达

4. SVA断言基础与复杂控制逻辑表达

在Jasper平台上做复杂控制逻辑的形式验证，SVA（SystemVerilog Assertion）是把“设计意图”翻译成“可被工具证明的时序命题”的核心语言。控制逻辑的难点通常不在组合条件本身，而在于条件之间的先后顺序、跨时钟沿的保持关系、以及多路请求与授权之间的互斥约束。SVA用序列（sequence）描述“一段时间内发生的事件模式”，用属性（property）描述“在什么条件下必须满足什么序列”，再通过蕴含操作符把二者绑定，从而把控制逻辑的时序要求写成可判定的断言。

序列与属性：从事件模式到时序命题

序列是时间轴上的事件模板。最基本的序列是单个布尔表达式，例如 req 表示在某个采样时刻 req 为真。序列可以通过延迟操作符 ##n 串联：req ##1 gnt 表示 req 成立后的下一个采样时刻 gnt 成立。重复操作符 [*n]、[->n]、[=n] 分别表示连续重复、非连续“goto”重复和带无关周期的重复，在描述“连续保持N拍”“第N次出现”这类控制语义时非常关键。例如 req[*3] 表示 req 连续三个采样时刻为真，而 req[->3] 只要求第三次出现，中间允许间隔。

属性则是对序列的时序约束。最简单的属性就是序列本身，但真正表达控制逻辑时通常使用蕴含：antecedent |-> consequent 表示“若前件在当前时刻成立，则同一时刻后件必须成立”（重叠蕴含）；|=> 表示“若前件成立，则下一采样时刻后件必须成立”（非重叠蕴含）。控制逻辑中大量“请求后下一拍必须授权”“错误标志置位后必须保持到清除”都适合用 |=> 表达。需要注意，蕴含的前件不成立时属性自动为真，这被称为“空洞成功”，在覆盖率分析中要单独关注，否则会误以为断言被充分验证。

时钟域指定与采样语义

SVA的时序推进依赖采样时钟。属性可以用 @(posedge clk) 指定时钟域，也可以在多时钟设计中用 @(posedge clk_a) ... |=> @(posedge clk_b) ... 描述跨时钟域关系。Jasper在elaborate阶段会为每个断言建立采样模型，因此必须明确：断言采样的是时钟沿到来前的稳定值，而不是沿之后的组合变化。若控制逻辑中存在异步复位，通常用 disable iff (rst_n == 0) 让断言在复位期间不参与检查，避免复位过程中的中间态造成误报。

跨时钟域断言要特别小心。假设 req 在 clk_a 域产生，ack 在 clk_b 域返回，直接写 @(posedge clk_a) req |=> @(posedge clk_b) ack 并不能保证两个时钟沿的对应关系，容易产生虚假反例。更稳妥的做法是先用同步器把信号同步到目标域，再在单一目标域内写断言，或者使用 $rose、$stable 等系统函数明确边沿与保持语义。

局部变量：把“同一笔事务”绑定起来

控制逻辑中经常需要断言“同一个请求的ID在授权时保持一致”“同一笔事务的地址在整条流水线中不变”。这类跨周期、跨阶段的数据一致性无法用纯布尔序列表达，需要局部变量。局部变量在序列中声明并赋值，例如：

property p_id_stable;
  logic [3:0] id;
  @(posedge clk) disable iff (!rst_n)
  (req, id = req_id) |=> (gnt |-> gnt_id == id);
endproperty

这里 (req, id = req_id) 是匹配项与赋值的组合：当 req 成立时，把当时的 req_id 存入局部变量 id；随后在授权时刻检查 gnt_id 是否等于该值。局部变量在每次序列匹配时重新绑定，因此天然支持流水线中多笔事务交错的情况。若同一周期有多笔请求，需要配合 first_match 或更精细的序列结构，避免变量被覆盖。

控制逻辑断言的典型表达

下面这张图把本节的核心要素组织成一条从“设计意图”到“可判定属性”的映射链，并标出序列、蕴含、时钟域和局部变量各自承担的角色。

把上述要素落到具体控制模块上，可以形成一组可执行的断言模板。以“请求—授权—完成”三阶段握手为例，假设 req 拉高后，授权 gnt 必须在1到3拍内出现，且授权期间 req 必须保持，完成后 done 拉高一拍：

// 授权及时性：req上升后1~3拍内必须gnt
property p_gnt_timely;
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:3] gnt;
endproperty

// 授权期间请求保持
property p_req_hold;
  @(posedge clk) disable iff (!rst_n)
  gnt |-> req;
endproperty

// 完成与授权配对，且ID一致
property p_done_id;
  logic [3:0] id;
  @(posedge clk) disable iff (!rst_n)
  (gnt, id = req_id) |=> ##[1:2] (done |-> done_id == id);
endproperty

在Jasper中加载这些属性后，prove -property 会尝试证明其恒真。若返回 cex（反例），波形会显示前件成立而后件失败的精确周期，通常对应控制逻辑中真实存在的时序漏洞，例如授权组合路径过长导致 gnt 晚于第3拍，或 req 在授权中途被上游撤销。若返回 proven，还需检查 cover 属性是否覆盖了前件成立的情形，否则断言可能因前件永假而“空洞通过”。

写控制逻辑断言时，先问三个问题：这件事的“起点事件”是什么？起点之后允许的时间窗口有多宽？窗口内哪些信号必须保持、哪些必须变化？把这三个答案分别映射到序列、延迟区间和蕴含后件，断言结构就基本确定了。

局部变量不能在属性外被其他属性共享，也不能在蕴含后件中重新赋值。若需要跨多个属性传递同一事务信息，应通过设计中的事务ID信号或辅助建模信号实现，而不是依赖SVA局部变量的全局可见性。

综合来看，SVA在复杂控制逻辑验证中的价值，是把“请求后多久授权”“同一事务ID是否贯穿”“互斥信号是否同时有效”这类时序约束，从人工波形检查转化为可被Jasper穷举证明或给出反例的数学命题。序列负责描述事件模式，属性负责表达约束，蕴含负责绑定条件与结果，时钟域负责确定采样时刻，局部变量负责跨周期绑定同一事务。五者配合，才能让控制逻辑的断言既准确又可判定。