SystemVerilog Assertion (SVA) 全面详解一、概述1.1 什么是断言断言 (Assertion)是一段描述设计预期行为的代码持续监视设计实际行为是否与预期一致一旦违背就报错。┌─────────────────┐ 设计行为 ──► │ 断言检查器 │ ──► 通过 ✅ / 失败 ❌ │ (Assertion Block)│ └─────────────────┘ ▲ │ 预期行为 (Specification)1.2 为什么需要 SVA对比项传统方式SVA错误发现时机仿真末尾看波形错误发生的当场立即报错错误定位难要回溯上千周期精确到周期代码量用 if/else 写检查逻辑冗长一行声明式描述可读性时序逻辑隐式隐藏直接对应规格描述复用性散落在 testbench可封装为 property 库覆盖率难统计支持 assertion 覆盖率1.3 SVA 的两大类类型关键字触发后行为Immediate Assertion立即断言assert在过程块中立即求值如if语句Concurrent Assertion并发断言assert property基于时钟周期持续求值SVA 核心二、立即断言Immediate Assertion立即断言在过程块initial/always/task中立即求值本质上是带报告功能的if。always (posedge clk) begin // 如果当前 valid 为高data 不能为 X assert (!valid || !$isunknown(data)) else $error(Data is X when valid is high); // 等价写法 if (valid $isunknown(data)) $error(Data is X when valid is high); end立即断言的三种变体// assert —— 仿真失败时报 fatal assert (condition) else $fatal(...); // assume —— 视为输入约束仿真形式验证都用 assume (condition) else $error(...); // cover —— 统计该断言被触发多少次 cover (condition) $display(Covered!);立即断言适合组合检查无时序并发断言才是 SVA 的核心能力。三、并发断言Concurrent Assertion基础3.1 基本结构assertion_label: assert property ((posedge clk) 条件) $info(通过); else $error(失败);关键点必须有时钟事件如(posedge clk)求值是周期同步的不会在中间翻转标签是可选的但强烈推荐带标签便于定位3.2 示例最简单的断言// 任何时候 req 为高下一拍 gnt 必须为高 req_gnt_check: assert property ((posedge clk) req | gnt) $info(ok); else $error(gnt not asserted one cycle after req);3.3 断言的三个层次// 1. assert property —— 检查必须成立不成立报错 check1: assert property ((posedge clk) req | gnt); // 2. assume property —— 假设输入满足此属性约束 // 验证 DUT 时假设激励满足此条件 input_assume: assume property ((posedge clk) req |- !gnt); // 3. cover property —— 统计该属性发生多少次覆盖率 cover_gnt: cover property ((posedge clk) gnt);四、序列Sequence—— 时序表达式断言的核心是描述时序关系而sequence是把一段时序封装起来的基本单元。4.1 基本序列sequence s_req_gnt; (posedge clk) req ##1 gnt; endsequence##1表示延迟 1 个时钟周期。整个序列表示req在某一拍为高下一拍gnt必须为高。4.2 延迟操作符##操作符含义##n延迟固定的 n 个周期##[m:n]延迟 m 到 n 个周期非确定##[*]延迟 0 到无穷个周期##[]延迟 1 到无穷个周期sequence s1; (posedge clk) a ##2 b; // a 后 2 拍 b endsequence sequence s2; (posedge clk) a ##[1:3] b; // a 后 1~3 拍内 b 出现 endsequence sequence s3; (posedge clk) a ##[*] b; // a 后任意拍 b 出现 endsequence4.3 蕴含操作符|-和|这是 SVA 最常用、最核心的操作符描述如果…那么…的因果时序。操作符含义说明-非交叠蕴含same-cycle交叠蕴含next-cycle// |- req 和 gnt 在同一拍 sequence s_overlap; (posedge clk) req |- gnt; endsequence // | gnt 在 req 下一拍 sequence s_nonoverlap; (posedge clk) req | gnt; endsequence蕴含语义如果蕴含前件不成立 → 断言空成功vacuously true不算失败如果前件成立 → 后件必须成立这就是如果 A 那么 BA 不发生时无需检查 B4.4 重复操作符操作符含义*n连续重复 n 次*m:n连续重复 m~n 次[*m:n]跟随式重复中间可以有其他信号[m:n]非连续重复goto 重复[-m:n]跳转到下一次匹配// a 连续 3 个周期为高 sequence s_consec; (posedge clk) a [*3]; endsequence // a 出现 2~5 次不要求连续中间可穿插其他 sequence s_goto; (posedge clk) a [2:5]; endsequence4.5 序列的与/或/非// 序列 A AND 序列 B —— 两序列的起点相同且都成功 seq_and: (a ##1 b) and (c ##1 d); // 序列 A OR 序列 B —— 任一成功即成功 seq_or: (a ##1 b) or (c ##1 d); // 序列 A 不出现 seq_not: not (a ##1 b);4.6 throughout 和 within// condition 在整个 seq 期间保持为真 sequence s_throughout; (posedge clk) condition throughout (a ##1 b ##1 c); endsequence // seq1 嵌套发生在 seq2 期间 sequence s_within; (posedge clk) (a ##1 b) within (c ##[1:5] d); endsequence4.7 first_match 和 intersect// first_match —— 只取第一个匹配避免多次匹配覆盖 sequence s_first; (posedge clk) first_match(a ##[1:5] b); endsequence // intersect —— 两个序列长度必须完全重合 sequence s_intersect; (posedge clk) (a ##[1:5] b) intersect (c ##2 d); endsequence五、属性Property—— 断言的容器sequence描述一段时序property把序列包装成可被assert/assume/cover使用的形式。5.1 property 的定义property p_req_gnt; (posedge clk) req | gnt; endproperty // 使用 req_gnt_check: assert property (p_req_gnt);5.2 disable iff —— 异步复位让断言在复位期间不进行检查避免复位时无数假错property p_req_gnt; (posedge clk) disable iff (rst_n 0) req | gnt; endproperty5.3 带参数的 property —— 提升复用property p_handshake(req_sig, ack_sig, delay); (posedge clk) disable iff (!rst_n) req_sig |- ##delay ack_sig; endproperty // 多处复用 check1: assert property (p_handshake(req, gnt, 1)); check2: assert property (p_handshake(read, ready, 3)); check3: assert property (p_handshake(dma_start, dma_done, 10));5.4 property 中的局部变量// 把当前 addr 存入局部变量等 ack 回来时检查地址一致 property p_addr_consistency; (posedge clk) req, local_addr addr |- // 在 req 拍捕获 addr ##[1:10] ack (addr local_addr); // ack 拍地址必须一致 endproperty:local_addr addr是 SVA 的局部变量赋值语法在序列起点捕获一个值后续使用。六、常用内建系统函数函数含义$rose(sig)信号从 0→1 的上升沿$fell(sig)信号从 1→0 的下降沿$stable(sig)信号保持不变$past(sig, n)信号 n 拍前的值默认 n1$past(sig, n, clk, gated)指定时钟与门控的过去值$onehot(sig)一次性只有一位为 1独热码$onehot0(sig)至多一位为 1$isunknown(sig)信号含 X 或 Z$countones(sig)信号中 1 的个数$count(sig, val)整个表达式中 val 的数量// 示例 seq1: assert property ((posedge clk) $rose(req) |- !gnt); // req 上升沿时 gnt 不能同时高 seq2: assert property ((posedge clk) state RUN |- $stable(mode)); // RUN 状态下 mode 不变 seq3: assert property ((posedge clk) valid |- !$isunknown(data)); // valid 时 data 不能 X七、完整实战案例7.1 案例一FIFO 满检查// FIFO 不能在 full 时再写入 property p_no_write_when_full; (posedge clk) disable iff (!rst_n) fifo_full |- !write_en; endproperty fifo_full_check: assert property (p_no_write_when_full); // FIFO 不能在 empty 时读出 property p_no_read_when_empty; (posedge clk) disable iff (!rst_n) fifo_empty |- !read_en; endproperty fifo_empty_check: assert property (p_no_read_when_empty);7.2 案例二握手协议// valid/ready 握手valid 一旦拉高必须保持到 ready 也拉高 property p_valid_stable; (posedge clk) disable iff (!rst_n) valid ~ready | valid; // valid 未握手成功则下一拍仍为高 endproperty valid_stable_check: assert property (p_valid_stable); // valid 一旦握手后必须撤除至少一拍防毛刺 property p_valid_drop_after_handshake; (posedge clk) disable iff (!rst_n) (valid ready) | !valid; endproperty valid_drop_check: assert property (p_valid_drop_after_handshake);7.3 案例三总线请求-授权-完成// req 后 1~16 拍内 gnt 必须出现gnt 后 1~32 拍内 done 必须出现 property p_req_to_done; (posedge clk) disable iff (!rst_n) req |- ##[1:16] gnt ##[1:32] done; endproperty req_to_done_check: assert property (p_req_to_done); // 同一时刻最多一个 outstanding property p_single_outstanding; (posedge clk) disable iff (!rst_n) req ~done |- !req; // 未完成时不能再发新 req endproperty single_outstanding_check: assert property (p_single_outstanding);7.4 案例四状态机检查// 状态机转移合法IDLE 只能 → REQ 或 IDLE property p_state_trans; (posedge clk) disable iff (!rst_n) $fell(rst_n) |- state IDLE; // 复位后必须是 IDLE endproperty reset_state_check: assert property (p_state_trans); // RUN 状态下不能直接跳到 DONE必须经过 WAIT property p_no_run_to_done; (posedge clk) disable iff (!rst_n) state RUN | state ! DONE; endproperty no_run_to_done_check: assert property (p_no_run_to_done);7.5 案例五独热码检查// 任何时候 priority selector 的输出必须是独热 property p_onehot; (posedge clk) disable iff (!rst_n) $onehot(sel_vector); endproperty onehot_check: assert property (p_onehot);八、SVA 在 UVM 中的应用8.1 在 interface / module 中放置 SVAinterface axi_if(input clk, input rst_n); logic [31:0] awaddr, awvalid, awready; logic [31:0] wdata, wvalid, wready; logic [1:0] bresp, bvalid, bready; // AXI 协议断言 property p_awvalid_stable; (posedge clk) disable iff (!rst_n) awvalid ~awready | awvalid; endproperty awvalid_stable_check: assert property (p_awvalid_stable); property p_b_valid_after_w; (posedge clk) disable iff (!rst_n) $rose(wlast wready) |- ##[1:32] bvalid; endproperty b_valid_check: assert property (p_b_valid_after_w); endinterface8.2 在 UVM 中收集 SVA 覆盖率// cover property 配合 covergroup cover_p_handshake: cover property ((posedge clk) req gnt); // 在 UVM 中读取 SVA 覆盖率 class my_test extends uvm_test; function void report_phase(uvm_phase phase); $display(SVA 覆盖率: %0.2f%%, $get_coverage()); endfunction endclass8.3 SVA 与 UVM report 机制联动通过$error/$fatal与 UVM 报告系统对接property p_check; (posedge clk) req | gnt; endproperty assert_check: assert property (p_check) uvm_info(SVA, req_gnt passed, UVM_HIGH) else uvm_error(SVA, gnt not asserted after req);注意在 SVA 的 pass/fail 分支中使用uvm_info/uvm_error宏需要这些宏在断言可见的作用域中通常放在 interface 或 module 而非 class 内。最干净的做法是把 SVA 放在 interface 中独立于 UVM class 体系。九、常见问题与最佳实践9.1 vacuous pass空成功蕴含的前件不成立时断言空成功不算失败也不算覆盖。要避免用空成功冒充覆盖率// ❌ 此 property 在 req 永不为高时永远 vacuous覆盖率统计虚假 cover_p: cover property ((posedge clk) req | gnt); // ✅ 同时分别 cover req 和 组合 cover_req: cover property ((posedge clk) req); cover_req_gnt: cover property ((posedge clk) req ##1 gnt);9.2 时钟与复位同时钟域的断言共用一个时钟几乎所有断言都要带disable iff (!rst_n)避免复位期间误报多时钟域断言要分别声明不要混用(posedge clk1)和(posedge clk2)9.3 性能影响断言会增加仿真开销每个断言每次求值模块级回归可以全开芯片级回归可关闭非关键断言// 关闭特定断言仿真选项 // assertcontroloff9.4 不该用 SVA 的场景场景替代方案数据完整性比对如 write→read 数据一致UVM scoreboard复杂协议的状态机覆盖UVM sequence coverage跨多事务的业务流程UVM sequence动态随机生成的场景组合UVM constrained randomSVA 擅长局部、时序、协议级的检查复杂业务流程用 UVM 更合适。9.5 推荐的断言组织项目目录结构: ├── rtl/ # RTL 源码 ├── tb/ │ ├── interfaces/ │ │ └── axi_if.sv # interface — 内含协议断言 │ ├── assertions/ │ │ └── sva_lib.sv # property 库可复用 │ └── ... └── ...把断言写在 interface 里是最常见也最推荐的做法与硬件信号最近可被多个 testbench 复用。十、SVA 速查表操作符速查操作符含义示例##n固定延迟 n 拍a ##1 b##[m:n]范围延迟a ##[1:3] b##[*]0~∞ 延迟a ##[*] b##[]1~∞ 延迟a ##[] b|-同拍蕴含req |- gnt|下一拍蕴含req | gnt[*n]连续重复 n 次a [*3][*m:n]连续重复 m~n 次a [*2:5][n]非连续重复a [2][-n]跳转到匹配a [-2]and/or序列与/或s1 and s2not序列非not s1throughout全程保持c throughout s1within嵌套发生s1 within s2intersect长度重合s1 intersect s2first_match首次匹配first_match(s1)if...else条件if (c) s1 else s2系统函数速查函数含义$rose(x)x 上升沿0→1, 0→X, X→1$fell(x)x 下降沿1→0, 1→X, X→0$stable(x)x 不变$past(x, n)n 拍前的 x$onehot(x)独热$onehot0(x)独热或全 0$isunknown(x)含 X/Z$countones(x)1 的个数十一、总结概念要点立即断言过程块内组合检查本质是带报告的 if并发断言SVA 核心基于时钟周期持续求值sequence描述一段时序的原子单元property把 sequence 包装为可断言的形式蕴含|-/|因果时序前件不成立则空成功disable iff异步复位期间不检查局部变量在序列起点捕获信号值供后续使用assert/assume/cover检查/约束/统计三种性质与 UVM 协同断言放 interfaceUVM 收集覆盖率SVA 的设计哲学把功能规格直接翻译成可执行代码。规格说req 后 1~10 拍内 gnt 必须为高就写成req |- ##[1:10] gnt一一对应可读、可仿真、可验证、可复用。它是 RTL 设计与验证之间最精确的契约语言也是覆盖率驱动验证中功能覆盖率的重要来源之一。在协议检查、握手验证、状态机合法性、独热码等场景中SVA 远比传统的 if 监控更简洁高效。