System Verilog学习笔记（二十一）——断言

SVA(SystemVerilog Aeesrtion)

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

分类

即时断言（immediate assertion）

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

并发断言（concurrent assertion）

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

建立SVA块

• 用sequence来表示单时钟或者多时钟求值的事件

sequence name_sequence
	......
endsequence

• 用property来表示复杂的有序行为

property name_property
	......
endproperty

• 属性（property）是仿真过程中被验证的单元，必须在仿真过程中被断言来发挥作用
• SVA提供了assert来检查属性

assertion_name:assert property(property_name);

建立SVA的步骤

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

序列内建方法

$rose(expression or signal)  //当信号/表达式由0变成1时返回真
$fell(expression or signal)  //当信号/表达式由1变成0时返回真
$stable(expression or signal) //当信号/表达式不发生变化时返回真

• 序列中的形式参数，使序列可以重用到设计中具有相似行为的信号上
• 时序检查：需要几个时钟周期才能完成的事件，SVA会用##来表示时钟周期延迟
• 在序列、属性和断言语句中都可以定义时钟，建议在属性中指定时钟，并保持序列独立于时钟，可以提高基本序列定义的可重用性

禁止属性（not）

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

蕴含操作符

• 蕴含等效一个if-then结构，只能用在属性定义中，左边叫做先行算子（antecedent），右边叫做后续算子（consequent）
• 先行算子是约束条件，当其成功时，后续算子才会被计算。如果先行算子不成功，整个属性默认为空成功。
• 交叠蕴含操作（|->）表示如果先行算子匹配，则在同一个周期计算后续算子的表达式
• 后续算子可以使用if_else语句

property p8;
	@(posedge clk) a|->b;
endproperty
a8:assert property(p8);  //p8检查a在给定时钟上升沿是否给高电平，如果为高，信号b在相同的时钟边沿也必须为高

• 非交叠蕴含操作（|=>）表示如果先行算子匹配，则在下一个周期计算后续算子的表达式

property p9;
	@(posedge clk) a|=>b;
endproperty
a9:assert property(p9);  //p9检查a在给定时钟上升沿是否给高电平，如果为高，信号b在下一个时钟沿也必须为高

描述延迟的方法

property p12;  //p12检查a&&b在任何给定时钟的上升沿为真
	@(posedge clk) (a&&b)|-> ##[1:3] c; 若表达式为真，则在接下来1-3个时钟周期内，信号c应该至少在一个时钟周期为高
endproperty
a12:assert property(p12);

• 在任何时钟上升沿，只能有一个有效的开始，但是可以有多个结束

无限时序窗口

• 在时序窗口的窗口上线可以使用$定义，表明时序没有上限，但是最好使用有限的时序窗口上限
• 检验器不停地检查表达式是否成功直到仿真结束

property p14;
	@(posedge clk) a|-> ##[1:$] b ##[0:$] c;  //无限
endproperty
a14:assert property(p14);

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);

$past构造

• SVA提供了一个内嵌的系统任务$past，可以得到信号在几个时钟周期之前的值。默认情况下，它提供信号在前一个时钟周期的值

$past(signal_name, number of clock cycles)

property p19;
	@(posedge clk) (c&&d)|->($past((a&&b),2)==1'b1);
endproperty
a19:assert property(p19);

连续重复运算符[*n]

• 表明信号或者序列将在指定数量的时钟周期内连续地匹配，信号的每次匹配之间都有一个时钟周期的隐藏延迟

signal or sequence [*n]

• 连续重复的次数也可以是一个窗口
• a[*1:5]表示信号a从某个时钟周期开始重复1-5次

跟随重复运算符[->]

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

非连续重复运算符[=]

• 表明在信号stop有效匹配的前一个时钟周期，信号a不一定需要有效的匹配

property p26;
	@(posedge clk) $rose(start) |->##2 (a[=3]) ##1 stop ##1 !stop; //a为高可以是连续的3个周期也可以是非连续3个，stop为高也可以与最后一个a为高间隔不止一个周期
endproperty

and构造

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

intersect构造

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

or构造

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

first_match构造

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

throughout构造

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

(expression) throughout (sequence)

within构造

• within允许在一个序列中定义另一个序列

seq1 within seq2 //表示seq1在seq2的开始到结束范围内发生，且seq2的开始点必须在seq1的开始点之前发生，seq2的结束点必须在seq1的结束点之后结束

SVA内建的系统函数

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

disable iff

• 在一些情况中，如果一些条件为真，则不应该执行检验，disable iff可以用来禁止在一些条件下的属性检验

disable iff (expr) <property>

expect构造

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

局部变量

• 在序列或者属性内部可以局部定义变量，而且对这种变量进行赋值
• 变量接着子程序放置，用逗号隔开
• 如果子序列匹配，那么变量赋值语句执行
• 每次序列被尝试匹配时，会产生变量的一个新的备份