第二章SVA 断言语言基础

SVA 断言的三种类型

SystemVerilog Assertions (SVA) 是 IEEE 标准的断言语言。在 FPV 中，SVA 用于编写属性来验证设计行为。

Assert（断言）

断言描述设计必须始终满足的行为。如果断言被违反，工具会产生反例。

Assume（假设）

假设约束输入环境。形式验证工具只考虑满足所有假设的输入序列。合理的假设是避免虚假反例（false failure）的关键。

Cover（覆盖）

覆盖点指定设计应该能到达的状态。如果覆盖点被击中（covered），说明该行为是可达的。

断言语法结构

一个典型的 SVA 断言模块如下（来自示例中的 v_arbiter.sva）：

example/.../v_arbiter.sva

module v_arbiter (
  clk, rstN,
  gnt, req,
  int_ready, int_valid, trans_started
);
input clk, rstN;
input [3:0] gnt, req;
input int_ready, int_valid, trans_started;

  // Assertion "grant_is_onehot0"
  //  Grant signal is one-hot or zero
  //
  property grant_is_onehot0;
    @(posedge clk) $onehot0(gnt);
  endproperty
  a_grant_is_onehot0: assert property (grant_is_onehot0);

  // Assertion "grant_is_one_cycle"
  //  Grant signal is high for one cycle only
  //
  property grant_is_one_cycle;
    @(posedge clk) (gnt!=4'b0) |=> (gnt==4'b0);
  endproperty
  a_grant_is_one_cycle: assert property (grant_is_one_cycle);

  // Functional coverage points
  //
  // Request
  c_req0: cover property (@(posedge clk) (req[0]));
  c_req1: cover property (@(posedge clk) (req[1]));
  c_req2: cover property (@(posedge clk) (req[2]));
  c_req3: cover property (@(posedge clk) (req[3]));
  //
  // Grant
  c_gnt0: cover property (@(posedge clk) (gnt[0]));
  c_gnt1: cover property (@(posedge clk) (gnt[1]));
  c_gnt2: cover property (@(posedge clk) (gnt[2]));
  c_gnt3: cover property (@(posedge clk) (gnt[3]));
  //
  // Control signals
  c_int_ready: cover property (@(posedge clk) (int_ready));
  c_int_valid: cover property (@(posedge clk) (int_valid));
  c_trans_started: cover property (@(posedge clk) (trans_started));
  //
  
  // Same functional coverage as above, described using covergroups
  covergroup cg @(posedge clk);
    c_req: coverpoint req {
      bins port[4] = {8, 4, 2, 1};
    }

关键语法元素

语法	含义
`@(posedge clk)`	在时钟上升沿评估
`\|->`	重叠蕴含（同一拍）
`\|=>`	非重叠蕴含（下一拍）
`##n`	延迟 n 个时钟周期
`[*n]`	重复 n 次
`$onehot0()`	系统函数：one-hot 或零
`$past()`	引用前一周期的值

Bind 机制

SVA 的 bind 语句允许将断言模块绑定到 RTL 模块上，无需修改 RTL 源码：

bind arbiter
  v_arbiter i_arbiter (
    .clk(clk), .rstN(rstN),
    .gnt(gnt), .req(req),
    .int_ready(int_ready),
    .int_valid(int_valid),
    .trans_started(trans_started)
  );

这将断言模块 v_arbiter 实例化到 arbiter 模块内部，信号按名称映射。

断言命名规范

a_*：assertion（如 a_grant_is_onehot0）
as_*：assumption（如 as_req_valid）
c_*：cover（如 c_req0）

VHDL + PSL 支持

JasperGold 也支持 VHDL 设计使用 PSL 语言编写断言：

-- PSL 断言示例
-- psl assert always (req -> next_e)) @(posedge clk);
-- psl assume always (req |-> not rst) @(posedge clk);

建议初学者从 SVA 开始学习，因为 SVA 与 SystemVerilog 设计语言紧密集成，是工业界最广泛使用的断言语言。

断言设计原则

学会 SVA 语法不等于会写好断言。写有效的断言是形式验证的核心技能。

好断言的特征

具体：检查明确的行为，不要过于宽泛（如"输出正确"太模糊，"grant 在 req 后 3 周期内拉高"才具体）
可证：在合理的时间和资源内可以被证明。无限时间窗的断言（如" eventually 某个信号会变高"）可能难以证明，需要加时间上限
覆盖边界条件：不仅检查正常路径，还要检查边界（空队列、满队列、复位期间等）
独立：一个断言检查一件事，不要把多个条件混在一个断言中

assert vs assume vs cover：三剑客分工

类型	用途	含义
`assert`	检查器	"这个性质必须始终成立"——如果违反，是 bug
`assume`	约束	"假设输入始终满足这个条件"——限制形式引擎的输入空间
`cover`	覆盖点	"这个场景应该能够到达"——验证约束不过强、确认设计能进入关键状态

黄金三角：每个关键功能应该同时有 assert（验证输出正确）、assume（约束输入合法）、cover（确认合法场景可达）。三者缺一不可。

bind 机制的优势

SVA 的 bind 指令允许将断言文件"绑定"到 RTL 模块实例上，而无需修改 RTL 源码：

// bindings.sva — 不修改 RTL 就能加断言
bind arbiter v_arbiter arb_bind_inst(clk, rstN, req, gnt);
//           ↑模块名  ↑断言模块  ↑实例名      ↑端口连接

好处：RTL 代码保持干净；同一套断言可以绑定到不同实例；断言可以独立版本管理。

常见断言错误

错误类型	症状	解决
断言太强	合法输入也触发 fail（假反例）	添加前提条件（antecedent \|-> consequent）
断言太弱	bug 漏过去了（假 proven）	增加检查条件，更精确描述预期行为
不可证	引擎永远超时	加时间窗限制、拆分为更小的断言
时钟错位	使用 `\|->` 而不是 `\|=>` 导致组合逻辑路径断言	理解重叠（\|->）和非重叠（\|=>）蕴含的区别

完整断言编写思路

确定协议：用自然语言写下要检查的设计行为（"当 req 拉高后，最多等 3 个周期 gnt 必须拉高"）
定义前提：什么条件下这个规则适用？（"当复位释放后且没有全局错误"）
描述后果：在前提满足时应该发生什么？
添加 cover：写一个 cover 属性确认这个场景确实能到达
写反例测试：故意造一个 bug 验证断言会 fail，确保断言真的在检查

来源文档

AN_scripting.pdf
example_jaspergold_apps/FPV/