第二章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)`	clocking event	clocking event 是 `posedge`/`negedge` 指示符与一个时钟信号的组合；表达式在每个 clocking event 上被检查
`\|->`	overlapping implication （重叠蕴含）	蕴含式左边是 antecedent（前提），右边是 consequent（后果）；后果与前提在同一拍求值
`\|=>`	nonoverlapping implication （非重叠蕴含）	后果在前提的下一拍求值
`##n`	cycle delay（周期延迟）	n 为非负整数。除 `##<num>` 外还支持 `##<constant id>`、`##(<expr>)`、`##[<left>:<right>]`、`##[<leftLim>:$]`；其中 expr / left / right 必须能求值为常量
`e[*n]`	consecutive repeat （连续重复）	连续重复 n 次。支持非负整数及区间 `<leftLim>:<rightLim>`、`<leftLim>:$`
`e[=n]`	nonconsecutive repeat （非连续重复）	非连续地重复 n 次，区间写法同上
`e[->n]`	goto repeat	"一直走到第 n 次成立为止"，区间写法同上
`$onehot0()`	Bit Vector System Function	evaluates all onehot values including 0——即 one-hot 或全零都算成立
`$past()`	Sampled Value System Function	引用之前若干拍的采样值。可带周期数参数，如 `$past(src, 2)` 表示前 2 拍；不写则为前 1 拍

工具相关的两点：①同属 Sampled Value System Function 的还有 $rose、$fell、$stable、$changed、$sampled；文档提示"在当前实现中，flop 在复位周期内不被驱动，其复位值由 reset analysis 决定"。②同属 Bit Vector System Function 的还有 $onehot、$countones、$isunknown。

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 模块内部，信号按名称映射。

断言命名规范

官方示例文件 v_arbiter.sva 里用的是这两个前缀：

a_*：assertion，如 a_grant_is_onehot0、a_grant_is_one_cycle
c_*：cover，如 c_req0、c_gnt

assumption 的前缀在这两个示例里没有出现——它们不含 assume。Cadence 自己的 Proof Accelerator 文档中用的是 asm_：

asm_my_tag_constant: assume property (@(posedge clk) $stable(my_tag));

这类前缀是工程惯例，不是工具强制要求。JasperGold 并不靠标签前缀区分属性类型——类型由 assert / assume / cover 关键字本身决定。统一前缀的实际好处是在 Property Table 里便于按名称过滤。

VHDL + PSL 支持

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

example/.../vhdl_psl/source/properties/v_arbiter.vhd.psl

vunit v_arbiter (arbiter(rtl)) {

  default clock is rose(clk);

  -- Assertion "grant_is_onehot0"
  --  Grant signal is one-hot or zero
  --
  property grant_is_onehot0 is onehot0(gnt);
  a_grant_is_onehot0: assert always grant_is_onehot0;

  -- Assertion "grant_is_one_cycle"
  --  Grant signal is high for one cycle only
  --
  property grant_is_one_cycle is (gnt/="0000")  -> next(gnt="0000");
  a_grant_is_one_cycle: assert always grant_is_one_cycle;

  -- Functional coverage points
  --
  -- Request
  c_req0: cover {req(0)};
  c_req1: cover {req(1)};
  c_req2: cover {req(2)};
  c_req3: cover {req(3)};

} -- v_arbiter

这是与前面 SVA 版本完全对应的 PSL 写法，可以对照着看清两种语言的差异：

概念	SVA	PSL
时钟声明	`@(posedge clk)` 写在每条 property 里	`default clock is rose(clk);` 在 vunit 里声明一次
蕴含	`\|->` / `\|=>`	`->`
下一拍	`\|=>`	`next(...)`
one-hot0	`$onehot0(gnt)`	`onehot0(gnt)`
覆盖点	`cover property (...)`	`cover {...}`
断言绑定	`bind` 语句	`vunit v_arbiter (arbiter(rtl))`

PSL 文件用 analyze -psl 读入（该开关用于分析没有内嵌在 RTL 里的 PSL，例如 vunit 文件）。

建议初学者从 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 源码：

example/.../verilog_sva/source/properties/bindings.sva

// bindings.sva — 不修改 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)
);

官方示例一律使用按名称连接（.port(signal)）而不是按位置连接。断言模块 v_arbiter 的端口顺序是 clk, rstN, gnt, req, int_ready, int_valid, trans_started，按位置连接时一旦顺序记错（例如把 gnt 和 req 写反）就会静默接错线，而按名称连接不会有这个风险。

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

常见断言错误

错误类型	症状	解决
断言太强	合法输入也触发 fail（假反例）	添加前提条件（antecedent \|-> consequent）
断言太弱	bug 漏过去了（假 proven）	增加检查条件，更精确描述预期行为
不可证	引擎永远超时	加时间窗限制、拆分为更小的断言
蕴含时序用错	consequent 的求值时刻比预期早一拍或晚一拍	分清两者：`\|->`（overlapping）让 consequent 与 antecedent 在同一拍求值，`\|=>`（nonoverlapping）让它在下一拍求值

完整断言编写思路

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

来源文档

AN_scripting.pdf
example_jaspergold_apps/FPV/
example_jaspergold_apps/designs/reference_design/verilog_sva/source/properties/（v_arbiter.sva、bindings.sva）
example_jaspergold_apps/designs/reference_design/vhdl_psl/source/properties/（v_arbiter.vhd.psl）
jaspergold_command_reference.pdf（analyze -psl）