SVA断言的用法教程

一、SVA是什么

SVA是System Verilog Assertion的缩写，即用SV语言来描述断言。断言是对设计的属性的描述，用以检查设计是否按照预期执行。

断言常用来验证总线时序或其他特定的时序逻辑，找出设计中的违例等。

断言可以分为立即断言和并行断言两种常见类型。

立即断言：非时序，执行时如同过程语句，可以在initial/always过程块或者task/function中使用。立即断言可以结合$fatal、$error、$warning、$info给出不同严重等级的消息提示。

格式如下，[ ]内为可选内容。

 

[name:]assert(expression) [pass_statement][else fail_statement];

 

//如果状态为REQ，但是req1或者req2均不为1时，断言将失败

always @ (posedge clk) begin

if(state == REQ)

assert(req1||req2) //立即断言

else begin

t = $time;

#5$error("assert failed at time %0t", t);

end

end

always @ (state)

assert (state == $onehot) else $fatal;

并行断言：时序性的，需要使用关键词property，与设计模块并行执行，并行断言只会在时钟边沿激活，变量的值是采样到的值。

立即断言很简单，无需赘述，本文主要讲述并行断言的用法。

二、SVA如何使用

SVA使用"assert"关键词来表示一个断言属性。而在进行对属性断言之前，我们需要进行属性(property)的声明。

 

property property_name;     ;endproperty

 

声明之后便可以对property进行断言，即 认为property中描述的属性为真，否则断言失败。

 

assertproperty(property_name);

 

以上是单独写一个property描述时序，然后assert调用它，对于较为简单的时序，也可直接在括号内写上property的内容。而对于较复杂的时序，也可以写定义序列sequence，再由sequence组成property.

SVA用在哪里呢？主要有2种：

直接嵌入RTL代码的module块中，通常用于设计人员；

module fifo(input clk, rst_n, read, output empty, ...)

//Actual FIFO code:

...

//Assertion: FIFO must not underflow

input_no_underflow: assert property( @(posedge clk) !(read && empty));

endmodule

对于验证人员，通常定义一个单独的sva模块，在其中进行property的声明和调用，然后和DUT或者平台顶层top进行绑定。module fifo_checker (input clk, rst_n, read, empty);

//FIFO must not underflow

input_no_underflow: assert property ( @(posedge clk) !(read && empty) );

endmodule

bind fifo fifo_checker fifo_checker_inst(.clk(clk),.rst_n(rst_n),.read(read),.empty(empty));

三、SVA语法简介

SVA具有层次结构，由低到高为布尔表达式-->序列sequence-->属性property，sequence描述的是一个时序过程，而property则是某种逻辑状态，或者多个时序过程应该符合的关系，也是我们要断言的对象。sequence和property的区别如下：

	sequence	property
层次	低层次，只能例化sequence	高层次，可以例化sequence和property
例化	直接调用	需要使用assert、cover、assume关键字
使用限制	不能使用蕴含操作符|-> |=>	可以使用蕴含操作符|-> |=>

对于较为简单的时序逻辑关系，可以不单独定义sequence，将sequence的内容直接写在property中；而对于时序关系较复杂的，或者为了提高复用性，可以将一些时序逻辑定义为单独的sequence，然后在property中调用。

logic clk = 0;

logic req,gnt;

logic a,b;

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence notype_seq (X, Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence withtype_seq (logic X, logic Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Property Specification Layer

//=================================================

property req_gnt_notype_prop(M,N);

@ (posedge clk) 

req |=> notype_seq(M,N);

endproperty

property a_b_type_prop(logic M, logic N;

@ (posedge clk) 

a |=> withtype_seq(M,N);

endproperty

//=================================================

// Assertion Directive Layer

//=================================================

req_gnt_notype_assert : assert property (req_gnt_notype_prop(req,gnt));

a_b_type_assert       : assert property (a_b_type_prop(a,b));

3.1 蕴含操作符

蕴含操作符只能在property中使用。

关键字	描述	说明
a |-> b	如果a成立，那么在当前时刻b必须成立	assertion成立的条件： 条件满足且结论为真 条件不满足（空成功）
a |=> b	如果a成立，那么在下一时刻b必须成立

3.2 延时操作符

用##操作符来表示延时。

关键字	描述	说明
a ##n b	a成立，且n个时钟周期后b成立
a ##[n:m] b	a成立，且n-m周期中任何一个时期b成立
a ##[*] b	a成立，且在当前周期到仿真结束的任何一个周期b成立，等价于##[0:$]	避免使用
a ##[+] b	a成立，且在下一周期到仿真结束的任何一个周期b成立，等价于##[1:$]	避免使用

logic clk = 0;

logic req,gnt;

logic a,b;

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence notype_seq (X, Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence withtype_seq (logic X, logic Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Property Specification Layer

//=================================================

property req_gnt_notype_prop(M,N);

@ (posedge clk) 

req |=> notype_seq(M,N);

endproperty

property a_b_type_prop(logic M, logic N;

@ (posedge clk) 

a |=> withtype_seq(M,N);

endproperty

//=================================================

// Assertion Directive Layer

//=================================================

req_gnt_notype_assert : assert property (req_gnt_notype_prop(req,gnt));

a_b_type_assert       : assert property (a_b_type_prop(a,b));

3.3 重复操作

关键字	描述	说明
a[*n]	a连续n个时钟周期成立
a [->n] b	a成立n次后（不要求连续），下一个时钟b成立
a [=n] b	a成立n次后（不要求连续），在后续任意时钟b成立

//连续3个时钟a均成立，则断言成功

property con_cycle1(a,b);

@ (posedge clk) a[*3];

endproperty

//a成立3次后(不要求连续)，在下一个时钟b成立则断言成功

property con_cycle2(a,b);

@ (posedge clk) a[->3]b;

endproperty

//a成立3次后(不要求连续)，b成立(后续任意一时钟)

property con_cycle3(a,b);

@ (posedge clk) a[=3]b;

endproperty

3.4 匹配操作

关键字	描述	说明
intersect(a,b)	a和b同时成立，且同时结束，则断言成功
a and b	a发生时b也发生（不要求同时结束），则断言成功	&& 只能连接两个表达式，而and可以连接两个sequence
a or b	a发生或b发生，则断言成功	|| 只能连接两个表达式，而or可以连接两个sequence
a within b	a发生的时间段内b也发生，则断言成功
a througnt seq	在序列seq成立的过程中，a事件一直成功
first_match(seq)	在seq第一次成功时检测，之后便不再检测

举例说明first_match(seq)的使用：

seq_a再clk 3 4 5时刻均满足，但是assert(first_match(seq_a))仅会在clk 3时成功匹配一次，之后便不再检测。

sequence seq_a;

a[*1:2] ##1 b[*2:3];

endsequence

property first_match_property;

first_match(seq_a);

endproperty

3.5 sequence 同步

默认情况下，多重sequence的组合是以后一个sequence的起始时间作为同步标志的，SVA提供ended结构以sequence的结束时间作为序列同步点。

若使用ended，则sequence必须定义时钟。关键字ended存储一个反映在指定时钟处序列是否匹配成功的布尔值。该布尔值仅在同一时钟内有效。

sequence s1;

@(posedge clk) a##1 b;

endsequence

sequence s2;

@(posedge clk) c ##1 d;

endsequence

property p1;

s1|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点

endproperty

property p2;

s1|=>##1 s2.ended; //s1成功匹配点滞后两个时钟周期是s2成功匹配点，即s1匹配成功则再过两个时钟周期s2必须匹配成功

endproperty

property p3;

s1.ended|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点

endproperty

property p4;

s1.ended|=> ##1 s2.ended;//s1成功匹配点滞后两个时钟周期是s2成功匹配点，即s1匹配成功则再过两个时钟周期s2必须匹配成功

endproperty

3.6内建函数

函数名	描述	举例
$onehot ()	只有1bit为1则返回1	assert property( @(posedge clk) $onehot0( {GntA, GntB, GntC} ) ) //任何时刻，有且仅有一个grant
$onehot0 ()	最大只有1bit为1，则返回1	assert property( @(posedge clk) $onehot0( {GntA, GntB, GntC} ) ) //任何时刻，最多只有一个grant
$countones ()	返回1的数量	assert property (@(posedge clk) $countones(Valid & Dirty) <=4 ) ) //dirty有效bit不超过4
$stable (boolean expression or signalname)	在时钟沿到来时，信号没有发生变化则返回1	assert property (@(posedge clk) !Ready |=> $stable(Data) ) //如果ready为0, Data必须保持不变
$past (signalname, nums)	将nums个周期之前的值赋给signalname nums默认缺省情况下，SVA提供前一个时钟沿处的信号值。	assert property( @(posedge clk) active |-> $past(cmd) != IDLE ) //如果active为1，cmd不能为IDLE
$rose (boolean expression or signalname)	在时钟沿到来时，信号跳变为1则返回1	assert property( @(posedge clk) Req |=> $rose(Valid) ) //req有效之后，vld必须为上升沿
$fell (boolean expression or signalname)	在时钟沿到来时，信号跳变为0则返回1	assert property( @(posedge clk) $fell(Done) |-> Ready ) //Done由1变0后，Ready须为有效

四、一些使用技巧

4.1 可变延时范围

延时操作或者重复范围（即 ##n 或 a[*n]）只可以使用常数，不可以使用变量。

如下的操作是非法的：

property variable_delay(cfg_delay);

@(posedge clk) disable iff (!rstn)

a ##cfg_delay b;

endproperty

但是如果我们还是想实现相同的可变延时，该怎么做呢？

可以定义一个seqence，间接实现相同的效果。

//delay sequence

sequence delay_seq(v_delay);

int delay;

(1,delay=v_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);

endsequence

//calling assert property

a_1: assert property(@(posedge clk) a |-> delay_seq(cfg_delay) |-> b);

使用delay_seq来替代变量cfg_delay. 下面解释这个seqence的实现：

首先定义了一个sequence内的局部变量，sequence内部是可以定义变量来做辅助逻辑表达的。

int delay                          ->  定义了一个整型变量 delay，用于存储当前的延迟时间。

(1,delay=v_delay)           -> 在序列的起始位置，生成一个事件 (1,delay=v_delay),这个事件表示，在第一个时钟上升沿时，将 delay 的值设置为 v_delay。

(1,delay=delay-1)            ->  (1,delay=delay-1) 表示在每个时钟上升沿时，将 delay 的值减 1。

first_match((1,delay=delay-1) [*0:$] ##0 delay <=0)   ->   对事件 (1,delay=delay-1) 重复若干次，直到delay的值为0. 此处相当是一个循环操作。

综上所述，这个序列表示：在第一个时钟上升沿时，将 delay 的值设置为 v_delay，然后每个时钟上升沿时，将 delay 的值减 1，直到 delay 的值小于等于 0。

4.2 Glue Logic

在验证或建模复杂行为时，引入辅助逻辑来观察和跟踪时间可以大大简化编码，这种辅助逻辑通常称为"glue logic".

如下的一个例子，对interface的SOP和EOP进行检查，DUT规范要求：

packets不能重合（SOP-EOP始终是匹配的）

允许单拍packet（SOP和EOP在同一cycle）

packet是连续的（SOP-EOP之间vld不能有缺口）

单纯用SVA编写的代码如下，可以发现比较复杂。

sequence sop_seen; //当sop出现后，该序列会持续成立

sop ##1 1'b1[*0:$];

endsequence

no_holes: assert property(//sop 到 eop之间的vld一直有效

sop |-> vld until_with eop

);

sop_first: assert property (vld && eop |-> sop_seen.ended); //eop之前或者当拍一定有sop

eop_correct: assert property(

not (!sop throughout ($past(vld && eop) ##0 vld && eop[->]) )

);

sop_correct: assert property(

vld && sop && !eop |=> not(!$past(vld && eop) throughout (vld && sop[->1]))

);

可已采用一些中间变量进行辅助，这样可以更简洁。

reg in_packet;//中间变量

always @(posedge clk) begin

if(!rstn || (eop&&vld) ) 

in_packet <= 1'b0;

else if (sop&&vld) in_packet <= 1'b1;

end

no_holes: assert property( //中间不能有空缺

in_packet |-> vld

);

eop_correct: assert property( //eop拍之前或者当拍一定有sop

vld && eop |-> in_packt || sop

);

sop_correct: assert property( //不会有重复sop拍

vld && sop |-> !in_packet

);