SV-assertion

断言(assert)是一种描述性语言，经过描述的指望结果来进行仿真验证。

断言有一个更加基础的信息，咱们称为属性(property)，属性能够做为断言结果，功能覆盖点，形式检查和约束随机激励生成。

断言相比较与testcase的仿真验证，对设计的可见度要求比较高，能够帮助快速定位错误的根源，断言能够分布在设计各个部位。

在项目中使用断言，有两种方式(eda tool中都支持)：

　　1) 使用预建的断言库，如OVL，

　　2) 使用SVA，PSL等断言语言来本身描述。(PSL是彻底独立的断言语言，SVA被继承在SV语言中)，

SVA的语言层次结构：

　　

assertion分为：

　　1) immediate assert，基于simulation event semantics；

　　　　　　assert/assume/cover (expression)  action_block；

　　2) concurrent assert，基于clock semantics；

　　　　　　assert/assume/cover (expression)  action_block；

　　action_block的声明：

　　　　　　statement | [statement] else statement；

　　immediate assert的action block紧跟着assert执行，就像在procedual block中，(好比active或者NBA region)

　　　　能够放在任何procedual中，initial，always，task，function。

　　concurrent assert的action block，在当前assert的reactive region执行，因此action block中使用$sampled()采样信号值，表示evaluate时的信号值。

 

assertion中的property，能够用来描述design的某一个行为，必须被例化在assert，assume，cover等编译选项后，

　　　　　　　　包含在module，interface，package，program，clocking，$unit中。

　　　　　　sequence，用来描述high level property的abort condition或者common start point，一系列的boolean expression。

 

在sva中，一个property表明一个thread，表示一系列event的sequence，可能持续多个cycle。

　　在property没有start的时候，thread不会起来，以后的check是不会被evaluation的。被认为是true的。

　　当该property执行结束或者结果已经出错，property在这个时间点结束。

SV引入了 |->表示overlapping的操做，resulting sequence (consequent) 与causing sequence (antecedent) 在同一个cycle完成。

　　　　  |=>表示non-overlapping的操做，resulting sequence在causing sequence的下一个cycle开始。

 

sequence：随着时间增长的SV boolean expression。

　　能够声明有formal args，local var；

　　method方法有：ended，matched，triggered，这三个方法都表示sequence的结束；

　　尽可能使用named sequence，来增长代码的可读性。

　　sequence支持的操做符：

　　　　

 

注意：1) sequence中的formal args是untyped的；formal args能够是一个signal，sequence，sequence method。

　　　2) sequence中的local var是不能用做setup delay或者repetition ranges的，

 

property：能够包含formal args，能够有local var；

　　　　

　　　　property支持的操做符：

　　　　　　

 

注意：1) 一个property_spec不是一个sequence，可是一个sequence能够是一个property_spec。

　　　2) formal args能够带default value。

 

SVA中支持的assertion 语句以及function：

　　

　　

　　

SVA中各个运算符之间的操做，能够是expression，sequence，property。

　　expression的优先级与logic operate部分相同。

　　sequence之间的优先级：

　　　　

　　property之间的优先级：

　　　　

 

verilog中的#表示延时，delay，##号表示延时若干个clock cycles。

若是implication operator中，antecedent fail，property被hold为vacuous success。

property中的not operator不能够和implication operator一同使用，通常只用在sequence组成的property，表示从不true的序列。

sequence中的first_match操做符，用来消除可能发生overlap的assert result：

　　1.若是property中只由一个sequence组成，则包含一个implicit first_match。

　　　　property p_seq;   (a##1 b ##[0:5] c); endproperty

　　2.consequent sequence中默认包含一个implicit first_match。

　　　　property p_seq;  a=>b##[1:2] c ## [0:4] d; endproperty

　　　　property p_seq;  a=>## [0:3] qABC.ended; endproperty

　　first_match主要用在antecedent的sequence中，一个sequence的ended是能够多触发的。

　　　　property p_seq; first_match(a##[2:3]b) |-> c;  endproperty

　　　　property p_seq; first_match(qABC.ended) |-> c; endproperty

重复操做符，能够用于sequence和expression中。

　　consecutive repetitive,  seq[*n], exp[*n]

　　non-consecutive repetive,   seq[=n],  exp[=n]

　　goto repetitive，non-consecutive exact repetitive， seq[->n]，exp[->n]

throughtout, condition over sequence。用来保证boolean condition在sequence有效期间是正确的。

　　 property p_seq; @(posedge clk)  $rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done); endproperty

　　　　　　其中enable throughout (ack ##[1:$] done)表示一个sequence；

　　　　　　##[1:4] seq表示一个sequence；

intersect, length-match sequence 表示两个sequence从同一个clock tick 开始而且在同一个clock tick结束。

within, 表示一个sequence在另外一个sequence有效中完成。

and, not-length-matching sequence，两个sequence同时开始，可是不须要同时结束。

sequence  method：

　　ended，主要用在sequence在single clock assertion中的endpoint；

　　　　ended method方法，在observe region以外是没有意义的，因此只能用在assert evaluation。

　　　　property p_seq;  @(psoedge clk) dmaWriteBlock(dma_done).ended |-> ##[1:5] cpu_interrupt; endproperty

　　matched，主要用在sequence在multi_clocks assertion中的endpoint；

　　　　将ended的结果进行latch and multi-clock sync，只在第一个clock的observe region有效。

　　　　sequence q_1(a, b);     @(posedge clk)   $rose(a) ##[2:3] b;     endsequence

　　　　sequence q_2;       @(posedge sysclk)   c##1 q_1(a,b).matched[->1]##1 d; endsequence

　　triggered，Level-sensitive control，主要用在disable iff，或者wait sequence.triggered中。

值采样函数，$stable(exp)，表示该exp的值与上一个clock tick的值相同。

　　property p_seq;    $fell(req_n) |=> ack ##1 $stable(ack)[*0:100] ##1data_valid;   endproperty。

assertion-ctrl system task；

　　$asserton,  $assertoff,  $assertkill。

assert cover中，能够收集assert更多的结果，主要分为coverage for properties，coverage for sequences。

　　1.coverage for properties, Number of times attempted, succeeded, failed, vacuous success.

　　2.coverage for sequence, Number of times attempted, matched.

 

assert中的clock定义：

　　1. sequence中定义，

　　　　顶层的clock定义不影响该sequence中的clock定义；

　　　　assert property中仍须要定义clock，该sequence中定义的clock不会变为property clock。

　　2. concurrent property中定义，

　　3. procedual block中inferred clock，

　　4. 自己property定义在clocking block中，

　　　　clocking block中的input output delay并不影响assert的执行，input，output delay只是对circuit delay的建模。

　　5. 定义default clocking，

　　6，声明assert的时候显式指定， assert property (@posedge clk) p_seq);

　　　　若是此时property中也定义了clock，两个clock必须相同。