当前位置: 首页 > news >正文

#SVA语法滴水穿石# (012)关于 first_match、throughout、within 的用法

我们今天学习, SystemVerilog 断言(SVA)中 first_matchthroughoutwithin 运算符。

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子序列完全包含在父序列中子序列的起止时间在父序列范围内子操作时间约束(如中断响应)

 


http://www.mrgr.cn/news/97227.html

相关文章:

  • Redis数据结构之List
  • 搭建K8S-1.23
  • Python菜鸟教程(小程序)
  • (二)使用Android Studio开发基于Java+xml的安卓app之环境搭建
  • Redis数据结构之String
  • vue2项目中,多个固定的请求域名 和 通过url动态获取到的ip域名 封装 axios
  • 量化交易----从0到1
  • 前端布局难题:父元素padding导致子元素无法全屏?3种解决方案
  • 增益调度控制 —— 理论、案例与交互式 GUI 实现
  • 【数学建模】(时间序列模型)ARIMA时间序列模型
  • #SVA语法滴水穿石# (013)关于内建系统函数
  • 实践:用Ollama+DeepSeek-R1搭建AI知识库
  • 博途 TIA Portal之1200做主站与200SMART的S7通讯
  • Axure RP9.0教程: 查询条件隐藏与显示(综合了动态面板状态切换及展开收缩效果实现)
  • C++ KMP算法
  • #SVA语法滴水穿石# (013)关于 disable iff、matched 、expect 的用法
  • 贪心算法之最小生成树问题
  • 分治-归并排序-逆序对问题
  • 【VUE】RuoYi-Vue3项目结构的分析
  • MessageQueue --- RabbitMQ WorkQueue