当前位置:   article > 正文

System Verilog学习笔记(二十一)——断言_systemverilig 断言sequence

systemverilig 断言sequence

SVA(SystemVerilog Aeesrtion)

  • 是一种描述性语言,可以完美地描述时序相关的情况。
  • 提供内嵌函数来测试特定的设计情况,且可以收集断言覆盖率

分类

即时断言(immediate assertion)

  • 基于仿真事件的语义
  • 测试表达式的求值像在过程块里其他表达式一样
  • 即时断言不是时序相关的,是立即被求值
  • 必须放在过程块的定义中
  • 只能用于动态仿真

并发断言(concurrent assertion)

  • 基于时钟周期
  • 在时钟边缘根据调用的变量采样值计算测试表达式
  • 可以放到过程块、模块、接口或程序的定义中
  • 可以在形式验证和动态仿真验证工具中使用

建立SVA块

  • 用sequence来表示单时钟或者多时钟求值的事件
sequence name_sequence
	......
endsequence
  • 1
  • 2
  • 3
  • 用property来表示复杂的有序行为
property name_property
	......
endproperty
  • 1
  • 2
  • 3
  • 属性(property)是仿真过程中被验证的单元,必须在仿真过程中被断言来发挥作用
  • SVA提供了assert来检查属性
assertion_name:assert property(property_name);
  • 1

建立SVA的步骤

  • 建立布尔表达式
  • 建立序列表达式
  • 建立属性
  • 断言属性

序列内建方法

$rose(expression or signal)  //当信号/表达式由0变成1时返回真
$fell(expression or signal)  //当信号/表达式由1变成0时返回真
$stable(expression or signal) //当信号/表达式不发生变化时返回真
  • 1
  • 2
  • 3
  • 序列中的形式参数,使序列可以重用到设计中具有相似行为的信号上
  • 时序检查:需要几个时钟周期才能完成的事件,SVA会用##来表示时钟周期延迟
  • 在序列、属性和断言语句中都可以定义时钟,建议在属性中指定时钟,并保持序列独立于时钟,可以提高基本序列定义的可重用性

禁止属性(not)

  • 属性检查的默认都是正确的条件,属性也可以被禁止发生。
  • 禁止属性表示期望属性永远是假,当属性为真时,断言失败

蕴含操作符

  • 蕴含等效一个if-then结构,只能用在属性定义中,左边叫做先行算子(antecedent),右边叫做后续算子(consequent)
  • 先行算子是约束条件,当其成功时,后续算子才会被计算。如果先行算子不成功,整个属性默认为空成功。
  • 交叠蕴含操作(|->)表示如果先行算子匹配,则在同一个周期计算后续算子的表达式
  • 后续算子可以使用if_else语句
property p8;
	@(posedge clk) a|->b;
endproperty
a8:assert property(p8);  //p8检查a在给定时钟上升沿是否给高电平,如果为高,信号b在相同的时钟边沿也必须为高
  • 1
  • 2
  • 3
  • 4
  • 非交叠蕴含操作(|=>)表示如果先行算子匹配,则在下一个周期计算后续算子的表达式
property p9;
	@(posedge clk) a|=>b;
endproperty
a9:assert property(p9);  //p9检查a在给定时钟上升沿是否给高电平,如果为高,信号b在下一个时钟沿也必须为高
  • 1
  • 2
  • 3
  • 4

描述延迟的方法

property p12;  //p12检查a&&b在任何给定时钟的上升沿为真
	@(posedge clk) (a&&b)|-> ##[1:3] c; 若表达式为真,则在接下来1-3个时钟周期内,信号c应该至少在一个时钟周期为高
endproperty
a12:assert property(p12);
  • 1
  • 2
  • 3
  • 4
  • 在任何时钟上升沿,只能有一个有效的开始,但是可以有多个结束

无限时序窗口

  • 在时序窗口的窗口上线可以使用$定义,表明时序没有上限,但是最好使用有限的时序窗口上限
  • 检验器不停地检查表达式是否成功直到仿真结束
property p14;
	@(posedge clk) a|-> ##[1:$] b ##[0:$] c;  //无限
endproperty
a14:assert property(p14);
  • 1
  • 2
  • 3
  • 4

ended结构

  • 序列可以简单的连接,即将多个序列以序列的起点作为同步点,来组合成时间上连续的检查
  • 使用序列的结束点作为同步点的连接机制
  • 既可以基于序列的起始点来同步序列,也可以基于序列的结束点来同步序列
sequence s15a;
	@(posedge clk) a ##1 b;
endsequence

sequence s15b;
	@(posedge clk) c ##1 d;
endsequence

property p15b;
	s15a.ended|->##2 s15b.ended;  //使用序列的结束点作为同步点的连接机制
endproperty

a15b:assert property (p15b);
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 7
  • 8
  • 9
  • 10
  • 11
  • 12
  • 13

$past构造

  • SVA提供了一个内嵌的系统任务$past,可以得到信号在几个时钟周期之前的值。默认情况下,它提供信号在前一个时钟周期的值
$past(signal_name, number of clock cycles)
  • 1
property p19;
	@(posedge clk) (c&&d)|->($past((a&&b),2)==1'b1);
endproperty
a19:assert property(p19);
  • 1
  • 2
  • 3
  • 4

连续重复运算符[*n]

  • 表明信号或者序列将在指定数量的时钟周期内连续地匹配,信号的每次匹配之间都有一个时钟周期的隐藏延迟
signal or sequence [*n]
  • 1
  • 连续重复的次数也可以是一个窗口
  • a[*1:5]表示信号a从某个时钟周期开始重复1-5次

跟随重复运算符[->]

property p25;
	@(posedge clk) $rose(start) |->##2 (a[->3]) ##1 stop;  //如果start信号在任何时钟上升沿拉高,那么两个时钟信号周期后,信号a连续或者间断出现3次为高,接着信号stop在下一个时钟周期为高
endproperty
  • 1
  • 2
  • 3

非连续重复运算符[=]

  • 表明在信号stop有效匹配的前一个时钟周期,信号a不一定需要有效的匹配
property p26;
	@(posedge clk) $rose(start) |->##2 (a[=3]) ##1 stop ##1 !stop; //a为高可以是连续的3个周期也可以是非连续3个,stop为高也可以与最后一个a为高间隔不止一个周期
endproperty
  • 1
  • 2
  • 3

and构造

  • 可以用来逻辑地组合两个序列,当两个序列都成功时,整个属性才成功。
  • 两个序列必须具有相同的起始点,但可以有不同的结束点
  • 检验的起始点是第一个序列的成功时的起始点,而检验的结束点是使得属性最终成功的另一个序列成功时的结束点

intersect构造

  • 两个序列必须在相同时刻开始且结束于同一时刻,也就是两个序列的长度必须相等

or构造

  • 只要一个序列成功,整个属性就成功

first_match构造

  • 可以确保只用第一次序列匹配,而丢弃其它的匹配
  • 当多个序列被组合在一起,first_match可以帮助在指定时间窗口内只选择第一次匹配

throughout构造

  • 当要求在检验序列的整个过程中,某个条件必须一直为真时,可以使用throughout操作符
(expression) throughout (sequence)
  • 1

within构造

  • within允许在一个序列中定义另一个序列
seq1 within seq2 //表示seq1在seq2的开始到结束范围内发生,且seq2的开始点必须在seq1的开始点之前发生,seq2的结束点必须在seq1的结束点之后结束
  • 1

SVA内建的系统函数

$onehot(expr)  //检验表达式满足“one-hot”,即表达式是否只有一位为1
$onthot0(expr) //检验表达式是否只有一位或者没有任何位为1
$isunknown(expr) //检验表达式任何位是否有X或Z
$countones(expr) //计算向量中为1的位数
  • 1
  • 2
  • 3
  • 4

disable iff

  • 在一些情况中,如果一些条件为真,则不应该执行检验,disable iff可以用来禁止在一些条件下的属性检验
disable iff (expr) <property>
  • 1

expect构造

  • expect语句等待的是属性的成功检验
  • expect构造后的代码是作为一个阻塞语句来执行的
  • expect语句允许在一个属性成功或失败后使用一个执行块

局部变量

  • 在序列或者属性内部可以局部定义变量,而且对这种变量进行赋值
  • 变量接着子程序放置,用逗号隔开
  • 如果子序列匹配,那么变量赋值语句执行
  • 每次序列被尝试匹配时,会产生变量的一个新的备份
声明:本文内容由网友自发贡献,不代表【wpsshop博客】立场,版权归原作者所有,本站不承担相应法律责任。如您发现有侵权的内容,请联系我们。转载请注明出处:https://www.wpsshop.cn/w/人工智能uu/article/detail/802706
推荐阅读
相关标签
  

闽ICP备14008679号