4序列操作符

 

1重复运算符

SVA语言提供三种不同的重复运算符：连续重复（consecutive repetition），跟随重复（go to repetition），非连续重复（non-consecutive repetition）。

连续重复

表明信号和序列将在指定数量的时钟周期内连续的匹配。信号的每次匹配之间都有一个时钟周期的隐藏延迟。连续重复的重复次数可以是一个窗口。

基本语法如下：

signal or sequence [*n] （n为表达式匹配的次数）

或者signal or sequence [*n:m] （表达式匹配的次数为n~m次）

例如：

property p5;

              @(posedge clk) $rose(start) |-> ##2 (a[*3]) ##2 stop ##1 !stop;

endproperty

其中a[*3]可以被展开成：

a ##1 a ##1 a

 

跟随重复

表明信号将匹配指定次数，但不一定在连续的时钟周期上发生。跟随重复的主要要求是信号的最后一个重复匹配发生在整个序列匹配前的那个时钟周期。

跟随重复的基本语法如下：

signal [->n]

 

非连续重复

表明信号将匹配指定次数，但不一定在连续的时钟周期上发生。非连续重复不要求信号的最后一个重复匹配发生在整个序列匹配前的那个时钟周期。

非连续重复的基本语法如下：

signal [=n]

下面举例说明跟随重复和非连续重复的区别：

property p6;

              @(posedge clk) $rose(start) |-> ##2 (a[->3]) ##1 stop ##1 !stop;

endproperty

property p7;

              @(posedge clk) $rose(start) |-> ##2 (a[=3]) ##1 stop ##1 !stop;

endproperty

 

 

    属性p6和p7做的检查为：在任何时钟上升沿start拉高后开始检查，两个时钟周期后，信号a连续或者间断的出现3次为高，接着信号stop在下一个时钟周期为高。p6与p7的唯一区别是，p6要求a第三次为高后的那个时钟周期stop必须为高，而p7只要求在a的第三个匹配之后，期望一个有效的信号stop，但不必在下一个时钟周期发生。

p6和p7都有一个未完成的检查，标记3s标出了检验器一个有效的开始，但在模拟结束前，a只重复为高两次，因而虽然信号stop出现了一次有效，但是模拟结束时这个检查未能完成。

 

2选择运算符

SVA允许在序列和属性中使用选择运算符。

例如

property p8;

            @(posedge clk) c ? d==a : d==b ;

endproperty

在信号c为高时，检验d是否与a相等；在信号c为低时，检验d是否与b相等。

 

.3二元运算符

（1） and运算符

二进制运算符and可以用来逻辑地组合两个序列。当两个序列都成功时，检验才成功。两个序列必须具有相同的起始点，但是可以有不同的结束点。检验的成功点是后一个成功的序列的匹配点。

例如：

sequence s9a;

       @(posedge clk) a ##[1:3] b;

endsequence

sequence s9b;

       @(posedge clk) c ##[2:3] d;

endsequence

sequence s9c;

@(posedge clk) s9a and s9b;

endsequence

property p9;

@(posedge clk) s9a and s9b;

endproperty

 

一个有效的检验开始于时钟周期2。在时钟周期3时，s9a第一次成功，但必须等待s9b也成功，整个序列的组合才成功。在时钟周期4时，s9b第一次成功，因此s9c和p9都成功，并且p9结束，但s9c继续检查，在时钟周期5检验到另一个成功。

 

（2）intersect运算符

二进制运算符intersect与and很相似，但它还要求两个序列必须在相同时刻开始且结束于同一时刻。

 

（3）or运算符

二进制运算符or可以用来逻辑地组合两个序列。两个序列必须具有相同的起始点，但是可以有不同的结束点。只要其中一个序列成功，检验就成功。检验的成功点是前一个成功的序列的匹配点。

 

4 first_match 构造

       使用了逻辑运算符（如and和or）的序列中如果指定了时间窗，就有可能出现同一个检验具有多个匹配的情况。first_match构造可以确保只用第一次序列匹配，而丢弃其他的匹配。这相当于在属性中定义这个相同的序列。

例如：

sequence s10a;

       @(posedge clk) a ##[1:3] b;

endsequence

sequence s10b;

       @(posedge clk) c ##[2:3] d;

endsequence

sequence s10c;

@(posedge clk) first_match(s10a or s10b);

endsequence

property p10;

@(posedge clk) s10a or s10b;

endproperty

序列s10c与属性p10做的是相同的检查，只保留s10a和s10b的第一次匹配。

5 throughout构造

  throughout构造可以保证某些条件在整个序列的验证过程中一直为真，其基本语法如下：

       (expression) throughout (sequence definition)

如果表达式没有在整个验证过程中保持为真，即使序列的其他检验都正确，也会导致整个检验失败。

6 within构造

within构造允许在一个序列中定义另一个序列。

其基本语法为：

seq1 within seq2

这表示seq1在seq2的开始到结束的范围内发生，且seq2的开始匹配点必须不晚于seq1的开始匹配点，seq2的结束匹配点必须不早于seq1的结束匹配点。

一个属性定义了设计的一个行为。一个属性可以作为一个假设、一个检查器或者一个覆盖率规范被用于验证。为了将这种行为用于验证，必须使用断言(assert)、假设（assume）或者覆盖(cover)语句。一个属性声明本身不会产生任何结果。

SVA中有七种类型的属性：

(1)   sequence：由序列构成；

(2)   negation：not property_expr；

(3)   disjunction：property_expr1 or property_expr2；

(4)   conjunction：property_expr1 and property_expr2；

(5)   if…else：

if(expression_or_dist)

       property_expr1

else

       property_expr2

(6)   implication：蕴含；

(7)   instantiation：属性的实例可以被用作property_expr或者property_spec。

property_expr ::= sequence_expr | implication_expr

property_spec ::= [clocking_event] [disable iff( expression )] [ not ] property_expr

       在序列、属性中都可以定义时钟。通常情况下， 在属性的定义中指定时钟，并保持序列独立于时钟是一种好的编码风格，这样可以提高序列的重用性。

       SVA提供了关键词disable iff来实现检验器的复位，即某些条件为真时，我们不想执行检验。其基本语法如下：

       disable iff (expression) <property definition>

       disable iff只可用在属性中。

例如：

property p_dis;

       @(posedge clk)

       disable iff(reset)  $rose(start) |=> a[=2] ##1 !start;

endproperty

SVA提供了下列系统函数来访问一个表达式的采样值。

(1)   $rose(boolean expression or signal_name)：

当信号/表达式的最低位变成1时返回真。

(2)   $fell(boolean expression or signal_name)：

当信号/表达式的最低位变成0时返回真。

(3)   $stable(boolean expression or signal_name)：

当信号/表达式不发生变化时返回真。

(4)   $past(signal_name, number of clock cycle,gating signal)：

得到信号在几个时钟周期之前的值。这个函数能够有效的验证设计到达当前时钟周期的状态所采用的通路是正确的。并且past可以由门控信号（gating signal）控制。

例如：property p_past;

              @(posedge clk) (c&&d) |->($past((a&&b),2,e)==1’b1);

         endproperty

当门控时钟e在任意给定的时钟上升沿有效时，检验如果表达式(c&&d) 为真，那么两个周期前，(a&&b)为真。

 

SVA还提供几个内建的函数来检查一些最常用的设计条件。

(1)   $onehot(expression)：在任意给定的时钟沿，表达式只有一位为高。

(2)   $onehot0(expression)：在任意给定的时钟沿，表达式只有一位为高或者没有任何位为高。

(3)   $isunknown(expression)：在任意给定的时钟沿，表达式的任何位是否是x或者z。

(4)   $onehot(expression)：在任意给定的时钟沿，计算向量中为高的位的数量。

2.8.1在序列和属性中使用形参

通过在序列中定义形参，相同的序列可以被重用到设计中具有相似行为的信号上。例如，我们可以定义下面的序列：

sequence s_lib1(a,b)

a||b;

endsequence

我们可以通过下面这个序列调用上面的序列：

sequence s_lib1_inst1

s_lib1(req1, req2);

endsequence

同样，与序列声明一样，一个属性在声明的时候可以带有可选的形式参数。当一个属性被实例化的时候，实参可以被传递到属性。通过使用实参替代形参，实参使得属性得到了扩展。例如，我们可以定义下面的属性：

property arb(a,b,c);

  @(posedge clk) $fell(a) |-> ##1 (c&&d)[*4] ##1 b;

endproperty

下面三个断言都可以调用属性arb：

a1_1:assert property(arb(a1,b1,c1,d1));

a1_2:assert property(arb(a2,b2,c2,d2));

a1_3:assert property(arb(a3,b3,c3,d3));

2.8.2使用参数的SVA检验器（module）

SVA检验器模块中可以使用参数，这为创建可重用的检验器模块提供了很大的灵活性。

SVA检验模块如下：

Module generic_chk(input logic a,b,clk)

parameter delay=1;

property p1;

  @(posedge clk) a |-> ##delay b;

endproperty

a1:assert property(p1);

endmodule

以下两个generic_chk的实例：

generic_chk #(.delay(2)) i1(a,b,clk); //将延迟参数改写为2个cycle

generic_chk i2 (c,d,clk);  //使用默认的1个cycle

 

在序列或者属性的内部可以局部定义变量。局部变量能够在需要的时候在一个序列或者属性实例中动态地产生并能在序列结束的时候移除。变量的赋值接着子序列放置，用逗号隔开。

例如：

sequence s0;

int lvar;

       @(posedge clk)

$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));

endsequence

序列在start拉高后开始有效的检查，序列中的局部变量lvar在每次enable匹配时，累加aa的值，并在序列结束匹配点处检查lvar是否与aout相等。

在上例中，局部变量在序列的实例中是不可见的。如果要使得子序列的局部变量可以被上层序列访问，必须声明一个局部变量并通过一个自变量传递到被实例化的子序列。

sequence s1(lvar);

     @(posedge clk)

$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));

endsequence

sequence s2;

int v1;

c ##1 s1(v1) ##1 (do1 == v1);

endsequence

任务、任务线程、void函数、void函数线程以及系统任务（tasks, task methods, void functions, void function methods, and system tasks）可以在一个序列成功匹配的结束处调用。子程序调用，出现在紧跟着序列的以逗号分割的列表中。

举例说明：

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

在序列s1中定义了局部变量v和w，当a为高电平时，把向量e的值赋给v；然后b出现一次高电平时，把向量f的值赋给w，并调用系统任务进行打印。

 

任务、任务线程、void函数、void函数线程以及系统任务（tasks, task methods, void functions, void function methods, and system tasks）可以在一个序列成功匹配的结束处调用。子程序调用，出现在紧跟着序列的以逗号分割的列表中。

举例说明：

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

在序列s1中定义了局部变量v和w，当a为高电平时，把向量e的值赋给v；然后b出现一次高电平时，把向量f的值赋给w，并调用系统任务进行打印。

 

SVA中提供了两种方法将一个复杂序列分解成较为简单的子序列。一种方法是以序列的起始点作为同步点，另一种方法是以序列的结束点作为同步点。后一种方法通过为序列名字追加上关键词ended来表示。

举例说明：

sequence s0;

@(posedge clk) a ##1 b;

endsequence

sequence s1;

       @(posedge clk) c ##1 d;

endsequence

property p0;

s0 |=>s1;

endproperty

property p1;

s0.ended |-> ##2 s1.ended;

endproperty

属性p0和p1做的是相同的检查。p0是以序列的起始点作为同步点，序列s1从s0匹配后的一个时钟周期开始检验；p1是以序列的结束点作为同步点，序列s1的结束匹配时间必须在s0的结束匹配时间之后的2个时钟周期。

 

使用ture表达式，可以在时间上延长SVA检验器，能够使得序列的结束点延长一个时钟周期。这可以用来实现同时监视多个属性且需要同时成功的复杂协议。

例如：

sequence s0;

@(posedge clk) a ##1 b;

endsequence

sequence s0_ext;

@(posedge clk) a ##1 b ##1 ‘true;

endsequence

sequence s1;

       @(posedge clk) c ##1 d;

endsequence

property p0;

@(posedge clk) s0.ended |-> ##2 s1.ended;

endproperty

property p1;

@(posedge clk) s0_ext.ended |=> s1.ended;

endproperty

属性p0和p1做的是相同的检查。序列s0_ext的成功匹配点比s0往后移了一个时钟周期。因此属性p0检查s0与s1成功匹配点是否相隔两个时钟周期，属性p1检查s0_ext与s1成功匹配点是否相隔一个时钟周期。

 

SVA允许序列或者属性使用多个时钟定义来采样独立的信号或者子序列。

2.13.1多时钟序列

多时钟序列由单时钟序列通过延迟连接符号##1连接而成。连接符号##1是非交叠的，并且能够同步不同子序列的时钟域。它表示从第一个单时钟序列的结束点，到第二个单时钟序列的起始点。当一个序列中使用了多个时钟信号时，只允许使用##1延迟构造。

例如：

sequence s_mul_clk;

       @(posedge clk1) a ##1 @(posedge clk2) b;

endsequence

序列s_mul_clk做的检查是：当信号a在时钟clk1的任意给定上升沿为高时，序列开始匹配，接着查找clk2的最近的上升沿，检查b是否为高。clk1的时钟周期3开始第一次有效的检查，查找clk2的最近的上升沿为其时钟周期2，检测到b为高，检查成功；clk1的时钟周期7开始第二次有效的检查，查找clk2的最近的上升沿为其时钟周期3，检测到b为低，检查失败。

多时钟序列只能用延迟连接符号##1连接单时钟序列。注意的是以下的序列都是非法的：

@(posedge clk1) s1 ##0 @(posedge clk2) s2

@(posedge clk1) s1 ##2 @(posedge clk2) s2

@(posedge clk1) s1 intersect @(posedge clk2) s2

 

2.13.2多时钟属性

多时钟属性的检查规则和多时钟序列相同。多时钟属性除了使用延迟连接符号##1，还可以对单时钟序列使用非交叠蕴含运算符。要注意的是，并不是不允许在多时钟序列中使用交叠蕴含运算符，只是不允许将其连接两个时钟定义不同的单时钟序列。例如，下面的语句就是合法的：

@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk1) s2

多时钟属性也可以使用逻辑运算符（and,or,not）连接两个单时钟序列。

2.13.3 matched构造

如果一个序列中定义了多个时钟，构造matched可以用来监测子序列的结束点。

例如：

sequence e1;

      @(posedge clk1) (a ##1 b ##1 c) ;

endsequence

sequence e2;

      @(posedge clk2) start ##1 e1.matched ##1 stop;

endsequence

 

信号start在clk2的时钟周期2为高，然后我们检测到序列e1在clk2的时钟周期3出现一次匹配，并且在clk2的时钟周期4信号stop为高，因此在clk2的时钟周期4出现序列e2的第一次成功；clk2的时钟周期5开始第二次有效的检验，但是在clk2的时钟周期6我们没有检测到序列e1的成功匹配点，因此在clk2的时钟周期6出现序列e2的失败。

理解matched构造的使用方法的关键在于，被采样到的匹配的值一直被保存到另一个序列最近的下一个时钟边沿。

 

SVA提供了关键词assert来检查属性，assert语句的基本语法是：

assertion_name: assert property(property_name);

执行块可以在属性成功或者失败后执行某些语句。

执行块的基本语法如下：

assertion_name:

       assert property (property_name)

                     <success message>;

               else

                     <fail message>;

执行块可以用来显示成功和失败。

 

有两种方法可以将SVA检验器连接到设计中：

（1）    在模块定义中内建或者内联检验器。

（2）    将检验器模块与模块、模块的实例或者一个模块的多个实例绑定。

检验器模块用来检验一组通用的信号，检验器可以与设计中任何的模块或者实例绑定。定义独立的检验器模块，增强了检验器的可重用性。

绑定的语法如下：

bind <module_name or instance_name>

      <checker name> <checker instance name>

                                  <design signals>;

举例说明绑定的使用：

下面为检验器模块的代码：

module mutex_chk(a,b,clk)

logic a,b,clk;

property p1;

       @(posedge clk) not(a&&b);

endproperty

endmodule

有如下所示的顶层模块：

module top(..);

inline u1(clk,a,b,in1,in2,ou1);

inline u2(clk,c,d,in3,in4,ou2);

endmodule

绑定的语句如下：

bind top.u1 mutex_chk i1(a,b,clk);

bind top.u2 mutex_chk i1(c,d,clk);

 

功能覆盖分为两类：对属性的覆盖和对序列的覆盖。

对属性覆盖的cover语句的结果包含下面的信息：

(1)   属性被尝试检验的次数

(2)   属性成功的次数

(3)   属性失败的次数

(4)   属性空成功的次数（由于使用蕴含）

例如得到如下的属性覆盖报告：

c0, 596 attempts, 202 match, 51 vacuous match（真正成功的次数为match的次数减去vacuous match的次数）

对序列覆盖的cover语句的结果包含下面的信息：

(1)   序列被尝试检验的次数（attemps）

(2)   所有成功的次数（total match）

(3)   初次成功的次数（first match）

(4)   序列空成功的次数（vacuous match）（总是为0，因为序列中不允许使用蕴含）

例如得到如下的序列覆盖报告：

c1, 596 attempts, 361 total match, 151 fisrt match, 0 vacuous match

序列中如果指定了时间窗，就有可能出现同一个检验具有多个匹配的情况。total match就包括了所有的成功，而first match只包括检验的第一次匹配。

 

SVA提供了关键词cover来衡量协议覆盖。其基本语法是：

cover_name: cover property (property_name or sequence_name);

 

通过运用cover语句我们可以得到属性或者序列的执行情况。我们可以把我们希望发生的情景表达成属性或者序列，并通过检测所有属性或者序列的检验至少真正成功一次，来实现功能覆盖。利用与assert语句中一样的执行块，我们可以控制模拟环境和收集功能覆盖数据。

下面以一个请求情景（Request Scenario）为例。

在任何给定的时间，有三个主控设备可以请求访问总线。这就意味着主控设备的req信号有七种可能的组合（0表示主控设备正在请求总线）。

测试平台应该生成上表中所有的输入组合。

 

七个属性定义了上表中的所有可能的请求组合。每个属性都与cover语句相连。我们期望每个请求组合都出现三次，因此我们只要检测七个属性是否都被成功检测到三次。并且，我们可以利用flag标志位来控制模拟环境，例如所有组合都检测到三次后就终止模拟。

要注意的是，每次属性或者序列的匹配都会执行action block在中的语句，如果在某一时钟周期同时产生了多个匹配，那么这个语句就会相应的被执行多次。

在形式验证和动态仿真中，assume语句将属性指定为环境中的假设。当一个属性被假设，工具会约束环境使得属性的检验得到满足。

在形式验证中，被假设的属性不会被强制满足检验。被假设的属性可以认为是被断言的属性的前提假设（hypothesis）。

在动态仿真中，环境必须被约束使得被假设的属性满足检验。和被断言的属性一样，被假设的属性也要被检查，并且在失败时报错。

       举例说明assume语句的使用：

检查信号req的属性如下：

property pr1;

@(posedge clk) !reset_n |-> !req; //when reset_n is asserted (0),keep req 0

endproperty

property pr2;

@(posedge clk) ack |=> !req; // one cycle after ack, req must be deasserted

endproperty

property pr3;

@(posedge clk) req |-> req[*1:$] ##0 ack;

// hold req asserted until and including ack asserted

endproperty

检查信号ack的属性如下：

property pa1;

@(posedge clk) !reset_n || !req |-> !ack;

endproperty

property pa2;

@(posedge clk) ack |=> !ack;

endproperty

在假设断言a1, assume_req1,assume_req2, and assume_req3一直满足的前提下，检查断言assert_ack1和assert_ack2是否满足检验。

a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;

assume_req1:assume property (pr1);

assume_req2:assume property (pr2);

assume_req3:assume property (pr3);

assert_ack1:assert property (pa1)

else $display(“\n ack asserted while req is still deasserted”);

assert_ack2:assert property (pa2)

else $display(“\n ack is extended over more than one cycle”);

    要注意的是assume语句不能使用执行块，因为执行语句对于假设来说没有意义。

SVA支持expect构造，它等待属性的成功检验，并将except构造后面的代码作为一个阻塞的语句来执行。expect语句允许在一个属性成功或者失败后使用一个执行块。

举例说明：

program tst;

initial begin

# 200ms;

expect( @(posedge clk) a ##1 b ##1 c ) else $error( “expect failed” );

ABC …

end

endprogram

上例中，在expect语句失败后打印失败信息，并且语句ABC要等待expect语句检验成功或者失败后才执行。