SVA断言
目录
Assertion介绍
什么是assertion?
- 用来与设计功能和时序做比较的属性描述。
- 断言可以用来完成:
1、检查设计的内容;
2、提高设计的可视度和调试能力;
3、检查设计特性在验证中是否被覆盖。 - 可读性好,因此也可用来服务于设计文档。
- 用来检查算法模型的断言在形式验证中可以穷尽计算,找出可能的违例。
- 可以自由地打开或关闭。
- 一小部分子集甚至可以用来综合或移植到emulation中,用来完成跨平台的移植。
断言覆盖率
- 仿真工具可以报告断言覆盖率,指示哪些断言没有被触发;
- 帮助检查是否验证计划捕捉到了所有需要的覆盖率;
- 断言覆盖率和功能覆盖率可以共同量化验证进度。
断言语言的发展与进步
- Verilog不支持断言,因此需要写过程语句来坐替代;
- SVA是由一些支持断言的语言进化而来,作为SV相对独立的语言分支。
类型划分
- 立即断言(immediate assertion):非时序的;执行时如同过程语句;可以在initial/always过程块或task/function中使用。
- 并行断言(concurrent assertion):时序性的;关键词property用于区分立即断言和并行断言;并行是因为它们与设计模块一同并行执行。
立即断言
[name:] assert (expression) [pass_statement] [else fail_statement]
time t;
always @(posedge clk)
if(staet == REQ)
assert (req1 || req2)
else begin
t = $time;
#5 $error("assert failed at time %0t", t);
end
//如果状态为REQ,但req1或req2均不为1时,断言将失败
立即断言可以结合$fatal/$error/$warning/$info
给出不同严重级别的消息提示。
always @(state)
assert (state == $onehot) else $fatal;
并行断言
base_rule1: assert property (cont_prop(rst,in1,in2)) pass_stat else fail_stat;
property req_grant_prop
@(posedge clk) req ##2 gnt ##1 !req ## !gnt;
endproperty
assert property req_grant_prop else $error("Req-Gnt Protocol violoation");
//Request-Grant协议描述:request拉高,两个周期后grant拉高
//一个周期后request拉低,一个周期后grant拉低
并行断言只会在时钟边沿激活,变量的值是采样到的值。
并行断言的执行阶段
并行断言的执行:
- 在preponed阶段采样稳定的变量值;
- 在obeserve阶段执行并行断言;
- 在reactive区域执行pass/fail语句。
通过这种方式可以保证并行断言执行会采样稳定的设计信号变量。
assertion,property,sequence
- assertion可以直接包含一个property;
- assertion也可以清晰地独立声明property;
- 在property内部可以有条件地关闭。
assert property(@(posedge clk)
disable iff (!rset)
a |=> b ##1 c);
assert property(my_prop);
property my_prop;
@(posedge clk)
disable iff(!reset)
a |=> b ##1 c;
endproperty
- property块可直接包含sequence;
- 复杂的property也可以独立声明多个sequence。
sequence s1;
@(posedge clk) a ##1 b ##1 c;
endsequence
sequence s2;
@(posedge clk) a ##1 c;
endsequence
property p1;
@(posedge clk) disable iff (!reset)
s1 |=> s2;
endproperty
sequences
- sequence用来表示在一个或多个时钟周期内的时序描述;
- 是property的基本构建模块,并经过组合来描述复杂的功能属性。
sequence用来提供下列的场景描述:
- 第一个时钟周期,第一个表达式成立;
- 接下来在若干时钟周期后,第二个表达式也成立;
- 以此类推,在接下来若干时钟周期,后续的表达式也成立。
sequence可以在module、interface、program、clocking块和package中声明。
- sequence可以提供形式参数,提高复用性:
sequence s20_1(data,en);
(!frame && (data==data_bus)) ##1 (c_be[0:3] == en);
endsequence
- 蕴含(implication)操作符用来表示如果property中左边的先行算子(antecedent)成立,那么property右边的后续算子(consequent)才会被计算。
- 如果先行算子不成功,那么整个属性就默认地被认为成功,即“空成功”(vacuous success).
- 蕴含结构只能用在属性定义中,不能在序列中使用。
交叠蕴含(|->):
- 如果条件满足,则评估其后续算子序列;
- 如果条件不满足,则表现为空成功,不执行后续算子。
非交叠蕴含(|=>):
- 如果条件满足,则在下一个周期评估其后续算子序列;
- 如果条件不满足,则表现为空成功,不执行后续算子。
sequence定义
基本操作符号
##
表示周期延迟符号,如##n表示在n个时钟周期后,##0表示在当前周期,即交叠周期。##[min:max]
表示在一个范围内的时钟周期延迟。min和max必须是非负数,序列会在从min到max时间窗口中最早的时间来匹配。$
用来表示无穷大的周期(在仿真结束前),但一般不建议这么做,这会增大仿真评估序列的负担。- 事件可以通过
[*n]
操作符来表示重复,n须为非负数且不能为$;类似的,也可使用[*m:n]
表示一定范围内的重复事件。 [=m]
用来表示一个事件的连续性,需要重复发生m次,但并不需要在连续周期内发生。类似的,也可使用[=m:n]
表示从最小m到最大n的重复发生的非连续周期次数。a[*0]
用来表示没有在任何正数时钟周期内有效。
and操作符号
- and用来表示两个序列需要保持匹配;
- 用法:
SEQ1 and SEQ2
下列情形将满足此操作符:
- 在从同一个起始点开始后,seq1和seq2均满足;
- 满足的时刻发生在两个序列都满足的周期,即稍晚序列的满足时刻;
- 两个序列的满足时间可以不同。
- 如果操作符两边的序列都是用来衡量采样信号而非事件时序,那么要求在相同周期内,and左右两边的序列都应该满足条件。
intersect操作符号
- 与and类似,但需要两边的序列时序在同一时钟周期内匹配。
or操作符号
- 表示两个序列至少需要有一个满足;
- 用法:
SEQ1 or SEQ2
下列情形将满足此操作符:
- seq1和seq2都从同一个时刻被触发;
- 最终满足seq1或seq2;
- 每个序列的结束时间可以不同,结束时间以序列满足的最后一个序列时间为准。
first_match操作符号
- 用来从多次满足的序列中选择第一次满足时刻,从而放弃其他满足的时刻。
sequence checkBusIdle;
(##[2:$] (frame && irdy));
endsequence
property first_match_idle
@(posedge clk) first_match(checkBusIdle) |-> (state==busidle);
endproperty
throughout操作符号
- 用来检查一个信号或一个表达式在贯穿(throughout)一个序列时是否满足要求。
- 用法:Sig1/Exp1 throughout Seq
- 例如,在burst模式信号拉低以后的两个周期时,irdy/trdy也应该在连续七个周期内保持为低,同时burst模式信号也应该在这连续周期内保持为低。
sequence burst_rule1;
@(posedge clk)
$fell(burst_mode) ##0
(!burst_mode) throughout (##2 ((trdy==0)&&(irdy==0)) [*7]);
endsequence
within操作符号
- 用来检查一个序列与另一个序列在部分周期长度上的重叠;
- 用法:
SEQ1 within SEQ2
- 例如,trdy需要在irday下拉的1个周期后保持7个周期为低,同时irday也将保持8个周期为低,以下序列会在第11个时钟周期满足:
!trdy[*7] within (($fell irdy) ##1 !irdy[*8])
if操作符号
- 可以在sequence中使用
if...else
- 例如,当master_req为高时,下个周期req1或req2应该为高;如果req1为高,则下个周期ack1为高;如果req2为高,则下个周期ack2为高:
property master_child_reqs;
@(posedge clk) master_req ##1 (req1 || req2)
if(req1)
(##1 ack1);
else
(##1 ack2);
endproperty
- 在cache访问时,如果有cache lookup满足,那么状态机的状态应该为READ_CACHE,否则应该为REQ_OUT:
property cache_hit_check
@(posedge clk) (state==CACHE_LOOKUP) ##1 (CHit||CMiss) |->
if(CHit)
##1 (state == CACHE_READ);
else
##1 (state == REQ_OUT);
endproperty
assert property(cache_hit_check) else $error;
检测序列的终点
- 用法:
SEQ.ended
- 在某一时刻,序列如果及时抵达终点,那么条件满足。
- 例如,在inst为高的下个周期,序列e1应该结束或已经结束:
sequence e1;
@(posedge sysclk) $rose(ready) ##1 proc1 ##1 proc2;
endsequence
sequence rule;
@(posedge sysclk) $reset ##1 inst ##1 e1.ended ##1 branch_back;
endsequence
- 在c拉起的下个周期,a拉低b拉高的序列也应该结束。
sequence aRbseq (aFell,bRose);
@(posedge clk) $fell(aFell) ##1 $rose(bRose);
endsequence
property endCycle;
@(posedge clk) $rose(c) |=> aRbseq(a,b).ended;
endproperty
//等价于
$rose(c)&&$fell(a)|=>$rose(b)
局部变量
- 可以在sequence或property中使用;
- 这些变量会伴随着sequence、property动态创建;
- 每个sequence实例都会有其自己的变量拷贝。
例如,在rdDone拉高后,读出的cache_rd_data会在2个周期后,在其基础上加1,并作reg_wr_data写入。
sequence rd_cache_done;
##[1:5] rdDone;
endsequence
sequence check_reg_wr_data;
int local_data;
(rd_cache_done,local_data=cache_rd_data) ##2 (reg_wr_data==(local_data+1));
endsequence
例如:如果read拉高,伴随着readId,则下一次read必须在这一次read对应的readAck返回之后才可以发起。
需要先记录上一次read的readId,继而在接下来的周期,检查没有相同readId的read发起,直到对应readId的上一次read的readAck拉起,并且readAckId与之相同。
property checkReadIdAck;
int loc_id;
($rose(read),loc_id=readId) |=>
not(($rose(read)&&readId==loc_id) [*1:$]) ##0 //##0相当于&&
($rose(readAck)&&readAckId==loc_id);
endproperty
调用方法
- 在序列匹配时,可以调用task、void function和系统函数;
- 例如,可以在s1序列末尾,分别打印出e和f变量被采样时的数值。
sequence s1;
logic v, w;
(a, v=e) ##1
(b[->1],w=f,$display("b after a with v = %h, w = %h\n",v,w));
endsequence
访问采样方法
一些系统函数可以用来访问指定类型的变量采样:
- 用来访问当前周期采样值;
- 用来访问上一个采样周期值;
- 用来检测采样变量的变化。
$rose(expression[, clocking_event])
和$fell(expression)[, clocking_event])
用来表示与上一个采样周期相比,变量最低位是否跳变为1或0,满足条件返回1,否则返回0。
clocking_event
在sequence中不需要单独提供,因为sequence中一般会指定采样时钟。
例如,在req拉起的2个周期以后,ack也应该拉高:
例如,在write_en拉低好(表征发起写访问),write_data的数据内容不应该为X:
$stable(expression[, clocking_event])
,用来表示在连续两个采样周期内,表达式的值保持不变,如果满足返回1,否则返回0。- 例如,在rd_en为高时,寄存器的值应该保持不变。
property reg_rd_data_stable;
@(posedge clk) rd_en |-> $stable(reg_data);
endproperty
$pase(expr[, num_cycles][, gating_expr][, clocking_event])
用来访问在过去若干采样周期前的数值。- 默认请客下,
num_cycles=1
,即采样1个周期前的数值。 - 例如,在ack拉高时的前两个周期,req信号应该为高:
property ReqCauseAck;
@(posedge clk) $rose(ack) |-> $past(req,2);
endproperty
- 例如,如果当前状态是CACHE_READ,那么上一个状态不应该是CACHE_MISS(如果cache丢失,那么无法从中读取数据):
property cache_read_chk;
@(posedge clk) (state==CACHE_READ) |-> ($past(state) != CACHE_MISS);
endproperty
$rose/$fell/$stable
也可以在过程块语句和连续赋值中使用。
always @(posedge clk)
TestDone <= stimulus_over & $rose(unit_done);
always @(posedge clk) begin
if($stable(my_sig)) begin
$display($time, "my_sig is stable from previous clk");
end
end
assign intr_cleared = $fell(intr, @(posedge clk);
assign intr_set = $rose(intr, @(posedge clk);
系统函数和方法
- 类似于访问采样的方法,还可以使用其他一些系统函数和方法,在sequence/property/assertion中使用:
$countbits(expression, control_bit)
用来计算expression中匹配control_bit数值的位数。$onehot(expression)
与$countbits(expression, '1)
一致,即计算expression中为1的位数。$isunknown(expression)
与$countbits(expression, '1)==1
一致,即检查expression中是否有且只有1位为1。$countones(expression)
与$countbits(expression, 'x, 'z)!=0
一致,即检查expression中是否有x或z。- 这些系统函数也可以用在一般的过程语句块和赋值语句中。
- 在assertion或property中,可以通过
disable iff
来给assertion做局部的条件控制。 - 全局控制方面,也可通过系统函数对property模块或实例做出控制:
$asserton
,默认控制,用来打开所有的assertion;$assertoff
,暂时停止assertion运行;$assertkill
,终止所有执行的assertion。
$assertoff(level, [list of module, instance or assertion_identifier]);
$assertkill(level, [list of module, instance or assertion_identifier]);
$asserton(level, [list of module, instance or assertion_identifier]);
level=0
,表示当前模块或层次下的所有assertion;level=n
,表示当前模块或层次下n层范围中的assertion;assertion_identifier
表示property的名字或assertion的label。
例如,在reset阶段停止所有的assertion,并在其复位之后,使能所有的assertion:
module assert_control();
initial begin: disable_assert_during_reset
@(negedge top_tb.reset_n) //active low reset
$display("Disabling assertion during reset");
$assertoff(0, top_tb.cpu_inst1);
@(posedge top_tb.reset_n)
$display("enabling assertions after reset");
$assertion(0, top_tb.cpu_inst1);
endmodule
Property使用
介绍
- 结合sequence对时序和逻辑的描述,property可用来描述设计的确切行为。
property可以在验证中用来做assumption、checker或coverage:
- 当使用
assert
关键词时,可以用作checker
来检查设计是否遵循property的描述; - 当使用
assume
关键词时,可以作为环境的假设条件,对于仿真环境和形式验证均起到对激励进行假设的作用; - 当使用
cover
关键词时,可以将property是否真正通过作为断言覆盖率来衡量。
property可以在module、interface、clocking块或package中
声明;也可以同sequence一样具备形式参数:sequence、negation、disjunction、conjunction、if...else、implication、instantiation
。
sequence
类型的property,只有当出现满足该sequence条件时,property才可以通过。negation
类型,即not_property_expr
。如果property_expr不满足,那么negation类型的property可以通过。
property rule2;
@(clkev) disable iff (foo) a |-> not(b ##1 c ##1 d);
endproperty
disjunction(OR)
用法即property_expr1 or property_expr2
,当至少一个property_expr满足时,property即通过。
property rule3;
@(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty
conjunction(AND)
,用法property_expr1 and property_expr2
,当两个property_expr均满足时,property通过。
property rule3;
@(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
endproperty
if(expression) property_expr1 else property_expr2
- implication蕴含,同sequence中用法一致,
sequence_expr {|->, |=>} property_expr
- instantiation用法即一个命名后的property可以在另外一个property_expr中所使用。
property rule6(x,y);
##1 x |-> y;
endproperty
property rule5a;
@(posedge clk)
a ##1 (b || c) [->1] |->
if(b)
rule6(d, e)
else // c
f;
endproperty
时钟声明
- 一般对于sequence或property,默认情况下在使用同一个时钟对数据做采样,但不排除多个时钟的采样情况。
@(posedge clk0) sig0 ##1 @(posedge clk1) sig1 // ##1的时钟对应的clk0
- 如果一个sequence或property需要声明多个时钟用来数据采样,可以使用
##1
结合第二个时钟沿采样,表示与第一个时钟(clk0)沿紧密相连的下个时钟(clk1)沿。 sequence
操作符号如and、or、intersect等无法被使用在多时钟sequence。- 以下的多时钟sequence声明均是非法的:
@(posedge clk1) s1 ##0 @(posedge clk2) s2
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2
property
中的and、or、not
则可以用在多时钟的property声明中,因为它们代表逻辑运算,并不参与sequence之间的时序关系。- 正常不会有这样的复杂场景,一般有多时钟的情况是写task(相当于checker)来解决。
- 如果clk0上升沿a为高,且下个clk1和clk2的上升沿,b和c分别为高时,该property成立。
- 可以在
sequence
中独立指定时钟:
sequence s2;
@(posedge clk) a ##2 b;
endsequence
property p2;
not s2;
endproperty
assert property(p2);
- 可以在
property
中独立指定时钟:
property p3;
@(posedge clk) a ##2 b;
endproperty
assert property(p3);
- 在过程块中,可以继承过程块的时钟:
always @(posedge clk) assert property (not (a ##2 b));
- 在时钟块中,也可以继承时钟块的时钟:
clocking master_clk @(posedge clk);
property p3;
not (a ##2 b);
endproperty
endclocking
assert property (master_clk.p3);
由此,断言的时钟由以下条件的优先级逐级判定:
- 显式声明断言时钟;
- 继承断言所嵌入环境的时钟;
- 继承默认的时钟。
对于并行断言,其必须具备时钟,即满足上述时钟条件之一。
对于多时钟的断言,必须显式声明时钟,无法继承或使用默认时钟;也无法嵌套入时钟块,同样也无法嵌套入由时钟驱动的过程块语句:
always @(clk) assert property (mult_clock_prop); // illegal
initial @(clk) assert property (mult_clock_prop); // illegal
绑定
- 断言既可以嵌入到设计中,也可以在设计外部定义。
- 嵌入到设计中,可能存在无法综合的问题,需同时考虑添加定向编译;在设计外部定义则不用担心综合问题。
- bind方法可以满足在设计外部定义断言,将其绑定到设计内部或接口上面:
bind design_block_or_instance_name block_with_assertions
- bind可以将包含断言的模块与设计模块或实例进行绑定,既可以满足对设计内部信号的可视性,又能够满足断言模块的独立性。
- 使用绑定的优势:无需修改原有设计代码,也无需添加监测信号,就可以实现断言的添加。
interface range (input clk, enable, input int minval, expr);
property crange_en;
@(posedge clk) enable |-> (minval <= expr);
endproperty
range_chk: assert property (crange_en);
endinterface
bind cr_unit range r1(c_clk, c_en, v_low, (in1&&in2));
expect语句
- 前面assert、assume和cover都是非阻塞的,而expect是阻塞的property使用方式;其语法与assert一致,不过它会等property执行通过,才会执行后续的语句。
- 即可以使用wait语句的地方,就可以使用expect语句:
expect_property_statement ::= expect(property_spec) action block
- 当期望一些特定时序的时候,作为阻塞条件,可以使用expect来嵌入到过程语句块中:
initial begin
#200ms;
expect(@(posedge clk) a ##1 b ##1 c) else $error("expect failed");
ABC:...
end
- 同assert语句的调用方式类似,它也可以使用在function和task中,同时也可以引用静态变量或动态变量:
integer data;
...
task automatic wait_for(integer value, output bit success);
expect (@(posedge clk) ##[1:10] data == value) success = 1;
else success = 0;
endtask
initial begin
bit ok;
wait_for(23,ok);
...
end