---

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 begint = $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) beginif($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 // cf;
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);endpropertyrange_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 beginbit ok;wait_for(23,ok);...
end