SVA断言简明使用指南 | 您所在的位置:网站首页 › sop写法 › SVA断言简明使用指南 |
目录 一、SVA是什么 二、SVA如何使用 三、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中描述的属性为真,否则断言失败。 assert property(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必须成立![]() 用##操作符来表示延时。 关键字 描述说明a ##n ba成立,且n个时钟周期后b成立a ##[n:m] ba成立,且n-m周期中任何一个时期b成立a ##[*] ba成立,且在当前周期到仿真结束的任何一个周期b成立,等价于##[0:$]避免使用a ##[+] ba成立,且在下一周期到仿真结束的任何一个周期b成立,等价于##[1:$]避免使用举例说明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默认情况下,多重sequence的组合是以后一个sequence的起始时间作为同步标志的,SVA提供ended结构以sequence的结束时间作为序列同步点。 若使用ended,则sequence必须定义时钟。关键字ended存储一个反映在指定时钟处序列是否匹配成功的布尔值。该布尔值仅在同一时钟内有效。 assert property( @(posedge clk) $onehot0( {GntA, GntB, GntC} ) ) //任何时刻,有且仅有一个grant $onehot0()最大只有1bit为1,则返回1assert property( @(posedge clk) $onehot0( {GntA, GntB, GntC} ) ) //任何时刻,最多只有一个grant $countones()返回1的数量assert property (@(posedge clk) $countones(Valid & Dirty) $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则返回1assert property( @(posedge clk) Req |=> $rose(Valid) ) //req有效之后,vld必须为上升沿 $fell(boolean expression or signalname)在时钟沿到来时,信号跳变为0则返回1assert 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 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 对事件 (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])) );可已采用一些中间变量进行辅助,这样可以更简洁。 参考资料: [1]SV之Assertions 断言_assert property_bleauchat的博客-CSDN博客 [2]http://systemverilog.us/vf/SolvingComplexUsersAssertions [3]SystemVerilog Variable delay in SVA - Verification Guide |
CopyRight 2018-2019 实验室设备网 版权所有 |