#SVA语法滴水穿石# （013）关于 disable iff、matched 、expect 的用法
SystemVerilog 断言（SVA）中 disable iff、matched 和 expect 的语法知识。
1. disable iff (condition)
功能与定义
-
作用：当指定条件（
condition）为真时，禁用当前属性的检查。-
常用于复位（
reset）期间忽略断言检查，避免误报。 -
条件生效时，断言立即停止检测，且不会触发失败。
-
语法：
property <property_name>;disable iff (condition) <property_definition>;
endproperty示例与波形
property check_valid_data;disable iff (reset) // 复位期间不检查@(posedge clk) valid |-> (data == expected_data);
endpropertyassert property (check_valid_data);波形分析：
周期： 0 1 2 3
reset :1 0 0 0
valid :0 1 1 0
data :X 5 6 5
expected_data:5 5 5-
周期 0：
reset=1，断言被禁用。 -
周期 1：
data=5，符合预期 → 断言通过。 -
周期 2：
data=6，不符合预期，但reset=0→ 断言失败。
2. matched
功能与定义
-
作用：用于 引用一个命名子序列的结束时间点，通常用于同步多个序列的时序关系。
-
结合
end关键字，捕获子序列的结束时间。 -
常用于多序列组合中需要对齐时序的场景。
-
-
语法：
sequence sub_seq;... // 子序列定义 endsequencesequence parent_seq;sub_seq.ended ... // 使用 matched 捕获子序列结束点 endsequence示例与波形
sequence req_ack_seq;req ##1 ack;
endsequencesequence data_transfer_seq;data_valid ##2 data_done;
endsequenceproperty check_sync;@(posedge clk) req_ack_seq.ended |-> data_transfer_seq.ended;
endpropertyassert property (check_sync);波形分析：
周期： 0 1 2 3
req :1 0 0 0
ack :0 1 0 0 // req_ack_seq 在周期1结束
data_valid:1 1 1 0
data_done :0 0 1 0 // data_transfer_seq 在周期2结束-
断言失败：
req_ack_seq在周期1结束，但data_transfer_seq在周期2结束，时序不同步。
3. expect
功能与定义
-
作用：类似于
assert，但 支持阻塞等待属性成功并执行后续操作。-
常用于测试平台（testbench）中，等待特定条件后继续执行代码。
-
可以指定超时时间，若超时则触发
else分支。
-
-
语法：
expect (<property_expression>) <action_on_success> else <action_on_failure>;示例与波形
initial begin// 等待 req 后 2 周期内收到 ack，超时则报错expect (@(posedge clk) req |-> ##[1:2] ack) $display("ACK received on time.");else $error("ACK timeout!");// 继续执行其他操作send_data();
end波形分析：
周期： 0 1 2 3 4
req :0 1 0 0 0
ack :0 0 1 0 0-
断言通过：
ack在周期2拉高（在req后 2 周期内）→ 打印成功消息。 -
超时场景：若
ack在周期3拉高，触发else分支报错。
4. 对比总结
| 关键字 | 核心作用 | 典型应用场景 |
|---|---|---|
disable iff | 条件触发时禁用属性检查 | 复位期间忽略断言 |
matched | 同步子序列的结束时间点 | 多序列时序对齐（如握手协议） |
expect | 阻塞等待属性成功并执行后续操作 | 测试平台中的条件等待与流程控制 |