#SVA语法滴水穿石# (012)关于 first_match、throughout、within 的用法
我们今天学习, SystemVerilog 断言(SVA)中 first_match
、throughout
、within
运算符。
1. first_match
定义与作用
-
功能:在可能产生 多个匹配结果 的复合序列(如
or
或重复操作符)中,仅选择第一个成功的匹配,忽略后续可能的匹配。 -
用途:避免因多个分支同时满足条件导致的重复触发,确保断言逻辑的确定性。
语法
first_match(sequence_expression);
示例与波形
sequence multi_match_seq;(req ##[1:3] ack) or (data_valid ##1 data_done);
endsequenceproperty check_first_match;@(posedge clk) first_match(multi_match_seq);
endpropertyassert property (check_first_match);
波形分析:
周期: 0 1 2 3 4
req : 1 0 0 0 0
ack : 0 1 0 0 0 // req ##1 ack 在周期1匹配
data_valid:0 0 1 0 0
data_done :0 0 0 1 0 // data_valid ##1 data_done 在周期3匹配
-
无
first_match
:断言在周期1和周期3均匹配成功,可能触发多次报告。 -
使用
first_match
:仅周期1的匹配被选中,周期3的匹配被忽略。
2. throughout
定义与作用
-
功能:确保 某个条件在整个序列的检测过程中持续为真。
-
若条件在序列的任一周期失效,断言失败。
-
-
用途:验证信号在特定操作期间保持稳定(如总线保持、电源稳定)。
语法
(condition) throughout sequence_expression;
示例与波形
sequence data_stable_seq;(data == $past(data)) throughout (req ##3 ack);
endsequenceproperty check_data_stable;@(posedge clk) req |-> data_stable_seq;
endpropertyassert property (check_data_stable);
波形分析:
周期: 0 1 2 3
req : 1 0 0 0
ack : 0 0 0 1
data : 5 5 5 5
-
断言通过:
data
在req
到ack
的周期内(0-3)始终保持不变。 -
失败场景:若
data
在周期2变为6,断言失败。
3. within
定义与作用
-
功能:表示 一个序列(
seq1
)必须完全包含在另一个序列(seq2
)的时间窗口内。-
seq1
的起始点 ≥seq2
的起始点。 -
seq1
的结束点 ≤seq2
的结束点。
-
-
用途:验证子操作在父操作的时间范围内完成(如中断响应必须在事务周期内)。
语法
seq1 within seq2;
示例与波形
sequence parent_seq;start ##5 end_signal;
endsequencesequence child_seq;sub_start ##2 sub_end;
endsequenceproperty check_within;@(posedge clk) child_seq within parent_seq;
endpropertyassert property (check_within);
波形分析:
周期: 0 1 2 3 4 5
start: 1 0 0 0 0 0
end_signal:0 0 0 0 0 1
sub_start:0 1 0 0 0 0
sub_end :0 0 1 0 0 0
-
断言通过:
child_seq
在周期1-3完成,完全包含在parent_seq
的周期0-5内。 -
失败场景:若
sub_end
在周期6拉高(超出parent_seq
窗口),断言失败。
4. 对比总结
运算符 | 核心作用 | 关键要求 | 典型应用场景 |
---|---|---|---|
first_match | 选择多个匹配中的第一个结果 | 序列可能多分支匹配 | 避免重复触发(如多模式选择) |
throughout | 确保条件在整个序列中持续有效 | 条件在序列所有周期内为真 | 稳定性检查(如数据保持) |
within | 子序列完全包含在父序列中 | 子序列的起止时间在父序列范围内 | 子操作时间约束(如中断响应) |