SystemVerilog断言（SVA）在接口协议检查中的实战写法
在芯片验证中，SystemVerilog Assertions（SVA） 是动态监测接口时序是否符合协议的利器。相比在testbench中写 if 判断，SVA能自动在仿真过程中报告违例，并精确指示发生时刻。本文以APB和AXI4-Lite为例，给出可直接复用的SVA断言模板。
一、SVA基本结构回顾
property name_of_property;
@(posedge clk) disable iff (!rst_n)
sequence_expr |-> consequence_expr;
endproperty
assert property(name_of_property);
• |->：重叠蕴含（前提成立时，同一时钟沿检查结论）
• |=>：非重叠蕴含（前提成立时，下一时钟沿检查结论）
二、APB协议检查实战
APB写传输的基本时序：PSEL 拉高 → PENABLE 拉高 → 下一周期完成。
2.1 PSEL与PENABLE不能同时拉低
property psel_penable_not_both_low;
@(posedge PCLK) disable iff (!PRESETn)
!(PSEL == 0 && PENABLE == 1); // 使能必须在选中时才有意义
endproperty
assert_psel_penable: assert property(psel_penable_not_both_low);
2.2 PENABLE必须在PSEL之后拉高
property penable_after_psel;
@(posedge PCLK) disable iff (!PRESETn)
$rose(PSEL) |=> ##0 PENABLE; // 下一周期PENABLE必须为高
endproperty
assert_penable_after_psel: assert property(penable_after_psel);
2.3 传输完成时PREADY必须为高
property pready_at_completion;
@(posedge PCLK) disable iff (!PRESETn)
(PSEL && PENABLE && PREADY) |=> $fell(PSEL); // 完成后退回IDLE
endproperty
assert_pready_at_completion: assert property(pready_at_completion);
三、AXI4-Lite协议检查实战
AXI4-Lite比APB复杂，关键是VALID与READY的握手规则。
3.1 AWVALID与AWREADY握手（地址通道）
// VALID不能依赖READY（VALID必须先拉高）
property awvalid_independent;
@(posedge ACLK) disable iff (!ARESETn)
$rose(AWVALID) |-> ##[1:$] AWREADY; // 最终必须收到READY
endproperty
assert_awvalid_independent: assert property(awvalid_independent);
// 一旦VALID拉高，必须保持直到READY为高
property awvalid_stable_until_ready;
@(posedge ACLK) disable iff (!ARESETn)
AWVALID && !AWREADY |=> AWVALID; // 下一周期VALID不能变低
endproperty
assert_awvalid_stable: assert property(awvalid_stable_until_ready);
3.2 写数据通道（WVALID与WREADY）
// WLAST必须在最后一笔数据时拉高
property wlast_with_last_data;
@(posedge ACLK) disable iff (!ARESETn)
WVALID && WREADY && WLAST |=> !WVALID; // 最后一笔后WVALID应撤
endproperty
assert_wlast_with_last_data: assert property(wlast_with_last_data);
3.3 写响应通道（BVALID与BREADY）
// 响应必须在地址和数据都完成后才发出
property bvalid_after_aw_and_w;
@(posedge ACLK) disable iff (!ARESETn)
BVALID |-> $past(AWVALID && WVALID && WREADY); // 简化：上一拍应有写请求
endproperty
assert_bvalid_after_aw_and_w: assert property(bvalid_after_aw_and_w);
四、调试技巧
4.1 用$error输出详细信息
assert property(@(posedge clk) disable iff (!rst_n)
req |-> ##[1:3] ack)
else $error("Req without ack within 3 cycles at time %0t", $time);
4.2 用cover统计覆盖率
cover property(@(posedge clk) $rose(PSEL) ##1 PENABLE);
// 确认APB传输是否发生过
4.3 层次化断言
将断言写在接口（interface）中，绑定到DUT，实现复用：
interface apb_assertions(input logic PCLK, PRESETn, PSEL, PENABLE, PREADY);
property psel_to_penable;
@(posedge PCLK) $rose(PSEL) |=> PENABLE;
endproperty
endinterface
bind dut apb_assertions u_apb_assert(.PCLK(PCLK), ...);
五、常见错误与规避
错误 原因 修正
断言在复位期间误触发 未加 disable iff (!rst_n) 在所有property中加入复位条件
|-> 与 |=> 用错 混淆重叠与非重叠蕴含 明确时序关系：同拍用 |->，隔拍用 |=>
断言一直不触发 序列表达式从未满足 用 cover property 确认前提是否出现过
仿真卡死 断言中 ##[0:$] 范围过大 限制最大延迟，如 ##[1:5]
六、结语
SVA断言的核心价值在于将协议规则转化为可自动检查的时序表达式。APB和AXI4-Lite的实践表明：抓住VALID/READY握手、PSEL/PENABLE时序、数据完成标志这几个关键点，就能覆盖大部分接口协议违例。将断言封装在interface中并通过bind注入DUT，是工程中最推荐的复用方式。
下载文档
