• 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时，断言将失败

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9

    立即断言可以结合$fatal/$error/$warning/$info给出不同严重级别的消息提示。

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

    • 1
    • 2

    并行断言

    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拉低

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6

    并行断言只会在时钟边沿激活，变量的值是采样到的值。
    在这里插入图片描述

    并行断言的执行阶段

    并行断言的执行：

    • 在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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9
    • 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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9
    • 10

    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

    • 1
    • 2
    • 3
    • 蕴含(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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6

    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

    • 1
    • 2
    • 3
    • 4
    • 5

    在这里插入图片描述
    在这里插入图片描述

    within操作符号

    • 用来检查一个序列与另一个序列在部分周期长度上的重叠；
    • 用法：SEQ1 within SEQ2
    • 例如，trdy需要在irday下拉的1个周期后保持7个周期为低，同时irday也将保持8个周期为低，以下序列会在第11个时钟周期满足：
    !trdy[*7] within (($fell irdy) ##1 !irdy[*8])

    • 1

    在这里插入图片描述

    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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 在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;

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8

    检测序列的终点

    • 用法：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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 在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)

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8

    在这里插入图片描述

    局部变量

    • 可以在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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7

    例如：如果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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6

    调用方法

    • 在序列匹配时，可以调用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

    • 1
    • 2
    • 3
    • 4
    • 5

    访问采样方法

    一些系统函数可以用来访问指定类型的变量采样：

    • 用来访问当前周期采样值；
    • 用来访问上一个采样周期值；
    • 用来检测采样变量的变化。

    $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

    • 1
    • 2
    • 3
    • $pase(expr[, num_cycles][, gating_expr][, clocking_event])用来访问在过去若干采样周期前的数值。
    • 默认请客下，num_cycles=1，即采样1个周期前的数值。
    • 例如，在ack拉高时的前两个周期，req信号应该为高：
    property ReqCauseAck;
	@(posedge clk) $rose(ack) |-> $past(req,2);
endproperty

    • 1
    • 2
    • 3
    • 例如，如果当前状态是CACHE_READ，那么上一个状态不应该是CACHE_MISS（如果cache丢失，那么无法从中读取数据）：
    property cache_read_chk;
	@(posedge clk) (state==CACHE_READ) |-> ($past(state) != CACHE_MISS);
endproperty

    • 1
    • 2
    • 3
    • $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);

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9

    系统函数和方法

    • 类似于访问采样的方法，还可以使用其他一些系统函数和方法，在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]);

    • 1
    • 2
    • 3
    • 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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9

    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

    • 1
    • 2
    • 3
    • disjunction(OR)用法即property_expr1 or property_expr2，当至少一个property_expr满足时，property即通过。
    property rule3;
	@(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty

    • 1
    • 2
    • 3
    • conjunction(AND)，用法property_expr1 and property_expr2，当两个property_expr均满足时，property通过。
    property rule3;
	@(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
endproperty

    • 1
    • 2
    • 3
    • 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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9
    • 10
    • 11

    时钟声明

    • 一般对于sequence或property，默认情况下在使用同一个时钟对数据做采样，但不排除多个时钟的采样情况。
    @(posedge clk0) sig0 ##1 @(posedge clk1) sig1 // ##1的时钟对应的clk0

    • 1
    • 如果一个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

    • 1
    • 2
    • 3
    • 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);

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 可以在property中独立指定时钟：
    property p3;
	@(posedge clk) a ##2 b;
endproperty
assert property(p3);

    • 1
    • 2
    • 3
    • 4
    • 在过程块中，可以继承过程块的时钟：
      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);

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6

    由此，断言的时钟由以下条件的优先级逐级判定：

    • 显式声明断言时钟；
    • 继承断言所嵌入环境的时钟；
    • 继承默认的时钟。

    对于并行断言，其必须具备时钟，即满足上述时钟条件之一。
    对于多时钟的断言，必须显式声明时钟，无法继承或使用默认时钟；也无法嵌套入时钟块，同样也无法嵌套入由时钟驱动的过程块语句：

    always @(clk) assert property (mult_clock_prop); // illegal
initial @(clk) assert property (mult_clock_prop); // illegal

    • 1
    • 2

    绑定

    • 断言既可以嵌入到设计中，也可以在设计外部定义。
    • 嵌入到设计中，可能存在无法综合的问题，需同时考虑添加定向编译；在设计外部定义则不用担心综合问题。
    • 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));

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7

    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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 同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

    • 1
    • 2
    • 3
    • 4
    • 5
    • 6
    • 7
    • 8
    • 9
    • 10
    • 11
  • 相关阅读:
    【0121】建立与postgres后端的连接（2）
    EE5805-Java-summary
    VIM指令
    com.google.guava:guava 组件安全漏洞及健康分析
    使用Spring Cloud设计电商系统架构
    分布式事务Seata源码解析11：全局事务执行流程之两阶段全局事务提交（手把手带你debug源码）
    机器学习笔记之最优化理论与方法(二)凸集的简单认识(上)
    【数据结构初阶】二、 线性表里的顺序表
    为什么没有办法画圆角？
    科普：什么是权益证明？
  • 原文地址：https://blog.csdn.net/weixin_41979380/article/details/126455596