SystemVerilog Assertion 设计、调试、测试总结（1）

1.5 一个简单的序列

序列s1检查信号“a”在每个时钟上升沿都为高电平。如果信号“a”在任何一个时钟上升沿不为高电平，断言将失败。

sequence s1;

@(posedge clk) a;

endsequence

1.6边沿定义的序列

序列s1使用的是信号的逻辑值。SVA也内嵌了边缘表达式，以便用户监视信号值从一个时钟周期到另一个时钟周期的跳变。这使得用户能检查边沿敏感的信号。三种这样有用的内嵌函数如下：

$rose(boolean expression or signal_name)    当信号、表达式的最低位变成1时返回真。

       $fell(boolean expression or signal_name)      当信号、表达式的最低位变成0时返回真。

       $stable(boolean expression or signal_name) 当表达式不发生变化时返回真。

序列s2检查信号“a”在每一个时钟上升沿都跳变成1。如果跳变没有发生，断言失败。

sequence s2;

@(posedge clk) $rose (a);

endsequence

1.10 SVA中的时钟定义

一个序列或者属性在模拟过程中本身并不能起什么作用。它们必须像下面的例子那样被断言才能发挥作用。

sequence s5;

@(posedge clk) a ##2 b;

endsequence

property p5;

       s5；

endproperty

a5: assert property (p5);

注意，序列s5中制定了时钟。这是一种把检查和时钟关联起来的方法，但是还有其他的方法。在序列、属性，甚至一个断言的语句中都可以定义时钟。下面的代码显示了在属性p5a的定义中指定时钟。

sequence s5a;

a ##2 b;

endsequence

property p5a;

       @(posedge clk) s5a；

endproperty

a5a: assert property (p5a);

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

断言的一个序列并不一定需要定义在一个独立的属性。因为断言语句调用属性，在断言的语句中可以直接调用被检查的表达式，如下面的断言a5b所示。

sequence s5b;

a ##2 b;

endsequence

a5b: assert property (@(posedge clk) s5b)

1.11禁止属性

在之前的所有例子中，属性检查的都是正确的条件。属性也可以被禁止发生。换句话说，我们期望属性永远为假。当属性为真时，断言失败。

序列s6检查当信号“a”在给定的时钟上升沿为高电平，那么两个时钟周期以后，信号“b”不允许是高电平，关键词“not”用来表示属性应该永远不为真。

sequence s6;

@(posedge clk) a ##2 b;

endsequence

property p6;

       not s6;

endproperty

a6: assert property (p6);

1.12一个简单的执行块

SystemVerilog语言被定义成每当一个断言检查失败，模拟器在默认情况下都会打印出一条错误信息。模拟器不需要对成功的断言打印任何东西。也可以使用断言陈述中的“执行块”（action block）来打印自定义的成功或失败信息。执行块的基本语法如下所示。

assertion_name:

assert property(property_name)

<success message>;

else

<fail message>;

下面显示的检验器a7在执行块中使用了简单的显示语句来打印成功和失败信息。

写法一：

sequence s7;

@(posedge clk) a ##2 b;

endsequence

property p7;

       s7；

endproperty

a7: assert
property (p7)

$display(“Sequence s7 successed\n”);

else

       $display(“Sequence s7 failed\n”);

写法二：

property p7;

              @(posedge clk) a ##2 b;

endproperty

a7: assert property (p7)

$display(“Property p7 successed\n”);

else

       $display(“Property p7 failed\n”);

执行块不仅仅局限于显示成功和失败。它可以有其他的应用，例如：控制模拟环境和收集功能覆盖数据。

1.13蕴含（Implication）操作符

蕴含等效于一个if-then结构。蕴含的左边叫做“先行算子”（antecedent），右边叫做“后续算子”（consequence）。先行算子是约束条件。当先行算子成功时，后续算子才会被计算。如果先行算子不成功，那么整个属性就默认地被认为成功。这叫做“空成功”（vacuous
success）。

蕴含结构只能被用在属性定义中，不能在序列中使用。

蕴含可以分为两类：交叠蕴含（Overlapped implication）和非交叠蕴含（Non-Overlapped implication）

1.13.1 交叠蕴含

交叠蕴含用符号“|->”表示。如果先行算子匹配，在同一个时钟周期计算后续算子表达式。

下面用一个简单的例子解释。属性p8检查信号“a”在给定的时钟上升沿是否为高电平，如果a为高，信号“b”在相同的时钟边沿也必须为高。

property p8;

              @(posedge clk) a |-> b;

endproperty

a8: assert property (p8);

当信号“a”检测为有效的高电平，而且信号“b”在同一个时钟沿也检测为高，这是一个真正的成功。若信号“a”不为高，断言默认地自动成功，则称之为空成功。相应的，失败指的是信号“a”检测为高且在同一时钟沿信号“b”未能检测为有效的高电平。

1.13.2 非交叠蕴含

交叠蕴含用符号“|=>”表示。如果先行算子匹配，在下一个时钟周期计算后续算子表达式。后续算子表达式的计算总是有一个时钟周期的延迟。

下面用一个简单的例子解释。属性p9检查信号“a”在给定的时钟上升沿是否为高电平，如果a为高，信号“b”在下一个时钟边沿为高。

property p9;

              @(posedge clk) a |=> b;

endproperty

a9: assert property (p9);

需要注意的是，断言在当前时钟周期开始，在下一个时钟周期成功的情况下才是真正的成功。相应的，如果属性有一个有效的开始（信号“a”为高），且信号“b”在下一个时钟周期不为高，属性失败。

1.13.3 后续算子带固定延迟的蕴含

属性p10检查如果信号“a”在给定时钟上升沿为高，在两个时钟周期后信号“b”应该为高。

property p10;

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

endproperty

a10: assert property (p10);

1.13.4 使用序列作为先行算子的蕴含

属性p10在先行算子的位置使用的是信号。先行算子同样可以使用序列的定义。在这种情况下，仅当先行算子中的序列成功时，才计算后续算子中的序列或者布尔表达式。在任何给定的时钟周期，序列s11a检查如果信号“a”和信号“b”都为高，一个时钟周期之后信号“c”应该为高。序列s11b检查当前时钟上升沿的两个时钟周期后，信号“d”应该为低。最终的属性检查如果序列s11a成功，那么序列s11b被检查。如果没有检测到有效的序列s11a，那么序列s11b将不被检查，属性检查得到一次空成功。

sequence s11a;

@(posedge
clk) 
(a && b) ##1 c;

endsequence

sequence s11b;

@(posedge
clk) 
##2 !d;

endsequence

property p11;

       s11a |-> s11b；

endproperty

a11: assert property (p11);

1.14 SVA检验器的时序窗口

到目前为止，带延迟的例子使用的都是固定的正延迟。下面，将讨论集中不同的描述延迟的方法。

属性p12检查布尔表达式“a&&b”在任何给定的时钟上升沿为真。如果表达式为真，那么在接下来的1~3个中周期内，信号“c”应该至少在一个时钟周期内为高。

SVA允许使用时序窗口来匹配后续算子。时序窗口表达式左手边的值必须小于右手边的值。左边的值可以为0。如果它是0，表示后续算子必须在先行算子成功的那个时钟沿开始计算。

property p12;

              @(posedge clk) 
(a&&b)  |->  ##[1:3] 
c;

endproperty 

a12: assert property (p12);

p12实际上以上面三个线程展开。

(a&&b)  |-> 
##1 c 或

(a&&b)  |-> 
##2 c 或

(a&&b)  |-> 
##3 c

属性有三个机会成功。所有三个线程具有相同的起始点，但是一旦第一个成功的线程将使整个属性成功。注意：在任何时钟上升沿只能有一个有效的开始，但是可以有多个有效的结束。这是因为每个有效的开始可以有三个机会成功。

1.14.1 重叠的时序窗口

属性p13与属性p12相似。两者最大的区别是p13的后续算子在先行算子成功的同一个时钟沿开始计算。

property p13;

              @(posedge clk)  (a&&b)  |-> 
##[0:3]  c;

endproperty

a13: assert
property (p13);

1.14.2无限的时序窗口

在时序窗口上限可以用“$”定义，这表明时序没有上限。这叫做“可能性”（eventuality）。检验器不停地检查表达式是否成功直到模拟结束。因为会对模拟器的性能产生巨大的负面影响，所有这不是编写SVA的一个高效的方式。最好总是使用有限的时序窗口上限。

property p14;

              @(posedge clk)  a |-> ##[1:$] b ##[0:$] c;

endproperty

a14: assert
property (p14);

1.16 使用参数的SVA检验器

SVA允许像Verilog那样在检验器使用参数（parameter）。两个信号间的延迟信息可以在检验器中用参数表示，那么这种检验器就可以在设计只有时序关系不同的情况重用。例子1.2显示了一个带延迟默认值参数的检验器。如果这个检验器在设计中被调用，它是以一个时钟周期作为延迟默认值。如果在实例化中重设检验器中延迟参数值，那么同一个检验器可以被重用。

module generic_chk(

input logic clk

);

parameter delay = 1;

reg a = 1'b0;

reg b = 1'b0;

always @(posedge clk)

begin

a <= $urandom_range(0,1);

b <= $urandom_range(0,1);

end

property p16;

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

endproperty

a16: assert property(p16);

endmodule

//call checker from the top.sv level module

generic_chk #(.delay(2)) i1(

.clk(clk)

);

generic_chk i2(

.clk(clk)

);

1.17 使用选择运算符的SVA检验器

SVA允许在序列和属性中使用逻辑运算符。属性p17检查如果信号“c”为高，那么信号“d”的值与信号“a”的相等。如果信号“c”不为高，那么信号“d”的值与信号“b”的相等。这是一个组合的检验，在每个时钟上升沿被执行。

property p17;

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

endproperty

a17: assert
property(p17);

1.18 使用true表达式的SVA检验器

使用true表达式，可以在时间上延长SVA检验器。这代表一种忽略的状态，它使得序列延长了一个时钟周期。这可以用来实现同时监视多个属性且需要同时成功的复杂协议。

序列s18a检查一个简单的条件。序列s18a_ext检查相同的条件，但是序列的成功被往后移了一个时钟周期。当这个序列被用在一个属性的先行算子时，它会造成一些差异。两个序列的结束点不同，因此开始检查后续算子的时钟周期也不一样。

`define true 1

sequence
s18a;

@(posedge
clk) a ##1 b;

endsequence

sequence
s18a_ext;

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

endsequence

sequence
s18b;

@(posedge
clk) c ##1 d;

endsequence

property
p18;

@(posedge
clk) s18a.ended |-> ##2
s18b.ended;

endproperty

property
p18_ext;

@(posedge
clk) s18a_ext.ended |-> ##2
s18b.ended;

endproperty

a18: assert
property (p18);

a18_ext: assert
property (p18_ext);

1.19 “$past”构造

SVA提供了一个内嵌的系统函数“$past”，它可以得到信号在几个时钟周期之前的值。在默认情况下，它提供信号在前一个时钟周期的值。结构的基本语法如下：

$past(signal_name, number of clock cycles)

这个任务能够有效地验证到达当前时钟周期的状态所采用的通路是正确的。

属性p19检验的是在给定的时钟上升沿，如果表达式（c&&d）为真，那么两个周期前，表达式（a&&b）为真。

property
p19;

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

  endproperty

a19: assert
property (p19);

带时钟门控的$past构造

“$past”构造可以由一个门控信号（gating singal）控制。比如，在一个给定的时钟沿，只有当门控信号的值为真时才检查后续算子的情况。使用门控信号的$past构造的基本语法如下：

$past(signal_name,
number of clock cycles，gating signal)

属性p20与属性p19相似。但是只有当门控信号“e”在任意给定的时钟上升沿有效时检验才被激活。

property p20;

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

endproperty

a20: assert property (p20);

1.21 重复运算符

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

连续重复---允许用户表明信号或者序列将在指定数量的时钟周期内都连续地匹配。信号的每次匹配之间都有一个时钟周期的隐藏延迟。

连续重复运算符的基本语法如下：

signal
or sequence [*n]

“n”是表达式应该匹配的次数。

比如，a[*3]可以被展开成：a ## 1 a ##1 a

而序列（a##1b）[*3]可以展开为：（a##1b）## 1（a##1b）## 1（a##1b）

跟随重复---允许用户表明一个表达式将匹配达到指定的次数，而且不一定在连续的时钟周期上发生。这些匹配可以是间歇的。跟随重复的只要要求是被检验重复的表达式的最好一个匹配应该发生在整个序列匹配结束之前。

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

signal [->n]

参考下面的序列：

start ##1 a[->3] ##1 step

这个序列需要信号“a”的匹配（即信号“a”的第三次，也就是最好以重复的匹配）正好发生在“stop”成功之前。换句话说，信号“stop”在序列的最后一个时钟周期匹配，而且在前一个时钟周期，信号“a”有一次匹配。

非连续重复---与跟随重复相似，除了它并不要求信号的最后一次重复匹配发生在整个序列匹配前的那个时钟周期。

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

signal [=n]

在跟随重复和非连续重复中只允许使用表达式，不能使用序列。

1.21.1连续重复运算符[*]

属性p21检查在检验有效地开始两个时钟周期后，信号“a”在连续的三个时钟周期为高，再过两个时钟周期，信号“stop”为高。下一个时钟周期，信号“stop”为低。

property
p21;

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

endproperty

a21: assert
property (p21);

1.21.2 用于序列的连续重复运算符[*]

属性p22检查有效开始的两个时钟周期以后，序列(a ##2
b)重复三次，接着再过两个时钟周期，信号“stop”为高。

property
p22;

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

endproperty

a22: assert
property (p22);

1.21.3 用于带延迟窗口的序列的连续重复运算符[*]

属性p23检查有效开始的两个时钟周期以后，序列(a ##[1:4]
b)重复三次，接着再过两个时钟周期，信号“stop”为高。实际上，这个序列有一个时序窗口，使得情况变得有些复杂。

property
p23;

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

  endproperty

a23: assert
property (p23);

主序列(a ##[1:4] b)[*3]可以被扩展成：

((a ##1 b) or (a ##2
b) or (a ##3 b) or (a ##4 b)) ##1

((a ##1 b) or (a ##2 b) or (a ##3 b) or
(a ##4 b)) ##1

((a ##1 b) or (a ##2 b) or (a ##3 b) or (a
##4 b))

1.21.4连续运算符[*]和可能运算符

属性p23指定了一个重复序列的时序窗口。同样的，重复的次数也可以是一个窗口。比如,a[*1:5]表示信号“a”从某个时钟周期开始重复1~5次。这个定义可以展开成下面的表达式。

a or

(a ##1 a) or

(a ##1 a ##1 a) or

(a ##1 a ##1 a ##1 a) or

(a ##1 a ##1 a ##1 a ##1 a)

重复窗口的边界规则与延迟窗口的相同。左边的值必须小于右边的值。右边的值可以是“$”，这表示没有重复次数的限制。

属性p24显示了一个带没有重复次数限制的有限的检查。它检验有效开始两个时钟周期后，信号“a”将保持为高，直到信号“stop”跳变为高。

property p24;

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

endproperty

a24: assert property (p24);

1.21.5 跟随重复运算符[->]

属性p25检查如果在任何时钟上升沿有效开始，两个时钟周期以后，信号“a”连续或者间断地出现3次为高，接着信号“stop”在下一个时钟周期为高。

property
p25;

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

endproperty

a25: assert
property (p25);

1.21.6非连续重复运算符[=]

属性p26检查如果在任何时钟上升沿有有效的开始信号，两个时钟周期后，在一个有效的“stop”信号前，信号“a”连续或者间断地出现3次为高，然后一个时钟周期后“stop”应该为低。p26和p25做的是相同的检查，唯一不同的是p26使用的是非连续（non-consecutive）重复运算符而不是跟随（go to）重复运算符。这表示在属性p26中，在信号“stop”有效匹配的前一个时钟周期，信号“a”不一定需要有有效的匹配。

property
p26;

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

endproperty

a26: assert
property (p26);

1.22 “and”构造

二进制运算符“and”可以用来逻辑地组合两个序列。当两个序列都成功时整个属性才成功。两个序列必须具有相同的起始点，但是可以有不同的结束点。检验的起始点是第一个序列的成功时候的起始点，而检验的结束点是使得属性最终成功的另一个序列成功时的点。

序列s27a和s27b时两个独立的序列。属性p27将两者用运算符“and”组合起来。当两个序列都成功时，属性成功。

sequence s27a;

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

endsequence

sequence s27b;

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

endsequence

property p27;

@(posedge clk) s27a and s27b
;

endproperty

a27: assert property(p27);

1.23 “intersect”构造

“intersect”运算符和“and”运算符相似，它有一个额外要求。两个序列必须在相同时刻开始且结束于同一时刻。换句话说，两个序列的长度必须相等。

属性p28检验与属性p27相同的情况。唯一的区别是它使用的是“intersect”构造而不是“and”构造。

sequence
s28a;

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

endsequence

sequence
s28b;

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

endsequence

property
p28;

@(posedge
clk) s28a intersect s28b ;

 endproperty

a28: assert property(p28);

1.24 “or”构造

二进制运算符“or”可以用来逻辑地组合两个序列。只要其中一个序列成功，整个属性就成功。

序列s29a和s29b时两个独立的序列。属性p29将两者用运算符“or”组合起来。当其中一个序列成功，整个属性就成功。

sequence
s29a;

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

endsequence

sequence
s29b;

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

endsequence

property
p29;

@(posedge
clk) s29a or s29b ;

endproperty

a29: assert
property(p29);

1.25 “first_match”构造

任何时候使用了逻辑运算符（如“and”和“or”）的序列中指定了时间窗，就有可能出现同一检验具有多个匹配的情况。“first_match”构造可以确保只用第一次序列匹配，而丢弃其他的匹配。当多个序列被组合在一起，其中只需时间窗的第一次匹配来检验属性剩余的部分时，“first_match”构造非常有用。

在下面的例子中，属性用运算符“or”将两个序列组合在一起。这个属性的几个可能的匹配如下所示。

a ##1 b;

a ##2 b;

c ##2 d;

a ##3 b;

c ##3 d;

当检验属性p30时，第一次匹配保留下来，其他匹配都被丢弃了。

sequence
s30a;

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

endsequence

sequence
s30b;

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

endsequence

property
p30;

@(posedge
clk) first_match (s30a or s30b) ;

endproperty

a30: assert
property(p30);

1.26 “throughout”构造

蕴含（implication）是目前讨论到的允许定义前提条件的一项技术。例如，要对一个指定的序列进行检验，必须某个前提条件为真。也有这样的情况，要求在检验序列的整个过程中，某个条件必须一直为真。蕴含只能在时钟沿检验前提条件一次，然后就开始检验后续算子部分，因此它不检测先行算子是否一直保持为真。为了保证某些条件在整个序列的验证过程中一直为真，可以使用“throughout”运算符。运算符“throughout”的基本语法如下所示：

（expression）throughout （sequence definition）

属性p31检查下列内容：

1. 在信号“start”的下降沿开始检查。
2. 检查表达式((!a&&!b)##1(c[->3])##1(a&&b))。
3. 序列检查在信号“a”和“b”的下降沿与信号“a”和“b”的上升沿之间，信号“c”应该连续或间断地出现3次为高电平。
4. 在整个检验过程中，信号“start”保持为低。

property
p31;

@(posedge
clk) $fell(start) |->(!start) throughout (##1 ( !a && !b ) ##1 (
c[->3] ) ##1 ( a&&b ) );

endproperty

a31: assert
property(p31);

1.27 “within”构造

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

seq1 within
seq2

这表示seq1在seq2的开始到结束的范围内发生，且序列seq2的开始匹配点必须在seq1的开始匹配点之前发生，序列seq1的结束匹配点必须在seq2的结束匹配点之前结束。       属性p32检查序列s32a在信号“start”的上升沿和下降沿之间发生。信号“start”的上升和下降由序列s32b定义。

sequence
s32a;

@(posedge clk) (( !a && !b ) ##1 (
c[->3] ) ##1 ( a&&b ) );

endsequence

sequence
s32b;

@(posedge
clk) $fell(start) ## [5:10] $rose(start);

endsequence

sequence
s32;

@(posedge
clk) s32a within s32b;

endsequence

property
p32;

@(posedge
clk) $fell(start) |-> s32;

endproperty

a32: assert
property(p32);

1.28 内建的系统函数

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

$onehot(expression)—检验表达式满足“one-hot”，换句话说，就是在任意给定的时钟沿，表达式只有一位为高。

$onehot0(expression)—检验表达式满足“zero one-hot”，换句话说，就是在任意给定的时钟沿，表达式只有一位为高或者没有任何一位为高。

$isunknown(expression)—检验表达式的任何位是否是X或者Z。

$countones(expression)—计算向量中为高的位的数量。

断言语句a33a检验向量“state”是“one-hot”,
断言语句a33b检验向量“state”是“zero one-hot”, 断言语句a33c检验向量“bus”是否有任何位为X或Z。断言语句a33b检验向量” bus”中等于1的位的个数大于1。

a33a:
assert property(
@ (posedge clk) $onehot(state) );

a33b: assert property(
@ (posedge clk) $onehot0(state) );

a33c: assert property(
@ (posedge clk) $isunknown(bus) );

       a33d: assert property(
@ (posedge clk) $countones (bus) );

1.29 “disable iff”构造

在某些设计情况下，如果一些条件为真，则我们不想执行检验。换句话说，这就像是一个异步的复位，使得检验在当前时刻不工作。SVA提供了关键词“disable iff”来实现这种检验器的异步复位。“disable iff”的基本语法如下：

disable iff (expression)  < property definition>

属性p34检查在有效开始后，信号“a”重复两次，且1个周期之后，信号“b”重复两次，再过一个时钟周期，信号“start”为低。在整个序列过程中，如果“reset”被检测为高，检验器会停止并默认地发出一个空成功的信号。

property
p34;

@(posedge
clk)

disable iff (reset)

$rose (start) |-> a[=2] ##1 b[=2]
##1 !start ;

endproperty

a34: assert
property(p34);

1.30 使用“intersect”控制序列的长度

运算符intersect提供了一个定义可能性运算符可以使用的最小和最大时钟周期数的机制。

属性p35定义了一个序列来检验在给定时钟边沿，如果信号“a”为高，那么从下一个时钟周期开始信号“b”最终将为高，接着在下一个时钟周期开始信号“c”最终也会为高。这个序列每当信号“a”为高时就开始，并且可能一直到整个模拟结束时才成功。

整个可以使用带1[*2:5]的intersect运算符来加以约束。这个intersect的定义检查从序列的有效开始点（信号“a”为高），到序列成功的结束点（信号“c”为高），一共经过2~5个时钟周期。

property
p35;

(@(posedge
clk) 1[*2:5] intersect (a ##[1:$] b ##[1:$] c));

endproperty

a35: assert
property(p35);

1.31 在属性中使用形参

可以用定义形参（formal arguments）的方式来重用一些常用的属性。属性“arb”使用了4个形参，并且根据这些形参进行检验。其中还定义了特定的时钟。SVA允许使用属性的形参来定义时钟。这样，属性可以应用在使用不同时钟的相似设计模块中。同样的，时序延迟也可以参数化，这使得属性的定义更具有普遍性。

属性首先检查有效开始。在规定的时钟上升沿，如果在信号“a”的下降沿后的2~5个时钟周期内出现信号“b”的下降沿，那么这就是一个有效开始。如果先行算子匹配，那么属性接着检查信号“c”和信号“d”的下降沿在下一个时钟周期出现，并且确保它们在4个连续的周期都保持为低。接着一个周期后，必须检测到信号“c”和信号“d”都为高，且再过一个时钟周期应该检测到信号“b”为高。

假定这是处理三个具有相似信号的不同主控设备的仲裁器的协议，可以很容易地重用前面定义的属性来检验所有3个主控设备的接口。

断言a36_1，a36_2和a36_3定义了每个主控接口用的检验器，分别使用了各个接口对应的信号作为属性arb的参数。

property arb
(a,b,c,d);

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

endproperty

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

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

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

1.32 嵌套的蕴含

SVA允许使用嵌套的蕴含。当我们有多个门限条件指向一个最终的后续算子时，这种构造十分有用。

属性p_nest检验如果信号“a”有一个下降沿，则是一个有效开始，接着在一个周期后，信号“b”，“c”和“d”应该为低电平有效信号以保持这个有效开始。如果第二个条件匹配，那么在6到10个周期内期望“free”为真。注意，当且仅当信号“b”,“c”和”d”都匹配时，在后续状况（consequent condition）“free”才会被检验是否为真。

`define free (a && b && c && d)

property p_nest;

@(posedge
clk) $fell (a) |-> ##1 (!b && !c && !d ) |-> ## [6:10] `free;

endproperty

a_nest: assert property(p_nest);

同一个属性可以被重写成不使用嵌套蕴含的方式，如下所示。

property p_nest1;

@(posedge
clk) $fell (a) ##1 (!b && !c && !d ) |-> ## [6:10] `free;

endproperty

a_nest1: assert property(p_nest1);

注意：

使用嵌套蕴含的属性p_nest中没有“else”情况，因此属性很容易就能重写成如p_nest1的形式。

1.33 在蕴含中使用if/else

SVA允许在使用蕴含的属性的后续算子中使用“if/else”语句。

属性p_if_else检查如果信号“start”的下降沿被检测到，就是一个有效开始，接着一个时钟周期后，信号“a”或者信号“b”为高。在现行算子成功匹配时，后续算子有两个可能的路径。

1. 如果信号“a”为高，那么信号“c”必须间歇地重复两次为高，且在下一个时钟周期，信号“e”必须为高。
2. 如果信号“a”不为高，那么信号“d”必须间歇地重复两次为高，且在下一个时钟周期，信号“f”必须为高。

注意，在检验信号“a”的后续算子中有优先级。

property p_if_else;

@(posedge
clk)   ($fell (start) ##1 (a ||
b)) |->

if (a)

(c[->2] ##1 e)

else

(d[->2] ##1 f);

endproperty

a_if_else: assert property(p_if_else);

1.34 SVA中的多时钟定义

SVA允许序列或者属性使用多个使用定义来采样独立的信号或者子序列。SVA会自动地同步不同信号或者子序列使用的时钟域。下面的代码显示了一个序列使用多个时钟的简单例子。

sequence
s_multiple_clocks;

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

endsequence

序列s_multiple_clocks检验在时钟“clk1”的任何上升沿，信号“a”为高，接着在时钟“clk2”的上升沿，信号“b”为高。当信号“a”在时钟“clk1”的任意给定上升沿为高时，序列开始匹配。接着“##1”延迟构造将检验时间移到时钟“clk2”的最近的上升沿，检验信号“b”是否为高。当在一个序列中使用了多个时钟信号时，只允许使用“##1”延迟构造。序列s_multiple_clocks不能被重写成下面这种形式。

sequence s_multiple_clocks;

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

endsequence

sequence
s_multiple_clocks;

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

endsequence

使用“##0”会产生混淆，即在信号“a”匹配后究竟哪个时钟信号才是最近的时钟。这将引起竞争，因此不允许使用。使用##2也不允许，因为不可能同步到时钟“clk2”的最近的上升沿。

       相似的技术可以用来建立有多个时钟的属性。如下面的例子所示：

property p_multiple_clocks;

@(posedge
clk1) s1 ##1 @(posedge clk1) s2;

endproperty

a_multiple_clocks: assert property(p_multiple_clocks);

它假定序列s1没有被时钟驱动，或者它的时钟定义和“clk1”一样。它又假定序列s2没有被时钟驱动，或者它的时钟定义和“clk2”一样。同样的，属性可以在序列定义之间使用非交叠蕴含运算符。下面是一个简单的例子：

property p_multiple_clocks;

@(posedge
clk1) s1 |=> @(posedge clk1) s2;

endproperty

禁止在两个不同时钟驱动的序列之间使用交叠蕴含运算符。因为现行算子的结束和后续算子的开始重叠，可能引起竞争的情况，这是非法的。下面的代码显示了这种非法的编码方式：

property p_multiple_clocks_implied_illegal;

@(posedge
clk1) s1 |-> @(posedge clk1) s2;

endproperty

1.35 “matched”构造

任何时候如果一个序列定义了多个时钟，构造“matched”可以用来检测第一个子序列的结束点。

序列s_a查找信号“a”的上升沿。信号“a”是根据时钟“clk1”来采样的。序列s_b查找信号“b”的上升沿。信号“b”是根据时钟“clk2”来采样的。

属性p_match验证在给定的时钟“clk2”的上升沿，如果序列s_a匹配，那么在一个周期后，序列s_b。

sequence s_a;

@(posedge clk1) $rose(a);

endsequence

sequence s_b;

@(posedge clk2) $rose(b);

endsequence

property p_match;

@(posedge clk2) s_a.matched |=> s_b;

endproperty

a_match: assert property (p_match);

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

1.36 “expect”构造

SVA支持一种叫“expect”的构造，它与Verilog中的等待和构造相似，关键的区别在于expect语句等待的是属性的成功检验。expect构造后面的代码是作为一个阻塞的语句来执行。expect构造的语法于assert构造很相似。expect语句允许一个属性成功或者是被后使用一个执行块（action block）。

使用expect构造的实例如下所示。

initial

begin

@(posedge clk);

#2ns cpu_ready =
1’b1;

expect (@(posedge clk) ##[1:16] memory_ready ==
1’b1)

$display(“Hand
shake successful\n”);

else

begin

$display(“Hand
shake failed: exiting\n”);

$finish();

for(i=0;
i<64; i++)

begin

send_packet();

$display(“Packet
%0d sent\n”,i);

end

end

注意，在信号“cpu_ready”被断言后，expect语句等待信号“memory_ready”在1~16个周期内的任意周期被断言。如果信号“memory_ready”如预期的被断言，那么显示一个成功信息，并且开始执行“for”循环代码。如果信号“memory_ready”没能如预期的被断言，那么显示错误信息，且模拟结束。

1.37 使用局部变量的SVA

在序列或者属性的内部可以局部定义变量，而且可以对这种变量进行赋值。变量接着子序列放置，用逗号隔开。如果子序列匹配，那么变量赋值语句执行。每次序列被尝试匹配时，会产生变量的一个新的备份。

property p_local_var1;

int lvar1;

@(posedge clk)  ($rose(enable1), lvar1 = a )  |=> ##4 (aa == (lvar1* lvar1* lvar1));

endproperty

a_local_var1
: assert property (p_local_var1);

属性p_local_var1 查找“enable1”的上升沿。如果找到，局部变量“lvar1”保存设计中向量“a”的值。在4个周期后，检查设计的输出向量“aa”是否与局部变量的值得立方相等。属性的后续算子等待设计满足延迟（4个时钟周期），然后将设计的实际输出和属性局部计算值比较。

可以在SVA中保持和操作局部变量，

property p_local_accum;

int lvar1;

@(posedge
clk) $rose(start) |=>(enable1 ## enable2, lvar1 = lvar1
+ aa )  [*4]##1 (stop && (aout == lvar1) );

endproperty

a_local_accum
: assert property (p_local_accum);

属性p_local_accum检查下列内容：

（1）在任意给定的时钟上升沿，如果检测到信号“start”的上升沿，标志一个有效开始。

（2）在一个周期后寻找一个特定的模型或者子序列。信号“enable1”必须被检测为高，且两个周期后，“enable2”应该被检测为高。这个子序列必须连续重复4次。

（3）在子序列的每次重复中，向量“aa”的值在序列内部被累加。在重复结束时，局部保存着向量“aa”累加4次的值。

（4）在重复结束的下一个时钟周期，期望信号“stop”为高，且局部变量保存的值与向量“aout”的值相等。

1.38 在序列匹配时调用子程序

SVA可以在序列每次成功匹配时调用子程序。同一系列中定义的局部变量可以作为参数传给这些子程序。对于系列的每次匹配。子程序调用的执行与它们在序列中的顺序相同。

sequence s_display1;

@(posedge clk) ($rose(a), $display(“Signal a arrive at
%t\n”,$time);

endsequence

sequence s_display2;

@(posedge clk) ($rose(b), $display(“Signal b arrive at
%t\n”,$time);

endsequence

property p_display_window;

@(posedge clk) s_display1 |-> ##[2:5]
s_display2;

endproperty

 a_display_window: assert property (p_display_window);

1.39将SVA与设计连接

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

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

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

有的工程师不喜欢在设计中加任何验证代码。在这种情况下，在外部绑定SVA检验器是很好的选择。SVA代码可以内建在模块定义的任何地方。

下面的例子显示了内联在模块中的SVA。

module inline(

input logic        clk ,

input logic        a  
,

input logic        b  
,

input logic  [7:0] d1 
,

input logic  [7:0] d2 
,

output logic [7:0] d

);

always @(posedge clk)

begin

if(a)

d <= d1;

if(b)

d <= d2;

end

property p_mutex;

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

endproperty

a_mutex: assert property (p_mutex);

endmodule

如果用户决定将SVA检验器与设计代码分离，那么就需要建立一个独立的检验器模块。定义独立的检验器模块，增强了检验器的可重用性。下面所示的是一个检验器模块的代码实例。

module
mutex_chk(

input logic        clk ,

input logic        a  
,

input logic        b

);

property p_mutex;

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

endproperty

a_mutex: assert property (p_mutex);

endmodule

注意，定义检验器模块时，它是一个独立的实体。检验器用来检验一组通用的信号，检验器可以与设计中任意的模块（module）或者实例（instance）绑定，绑定的语法如下所示：

bind <module_name
or instance_name > <checker name > <checker instance name >
<design siganls>

在上面的检验器例子中，绑定可以用下面的方式实现，

bind inline
mutex_chk i2 (a,b,clk);

在实现绑定时，使用的是设计中的实际信号。

比如，我们有一个如下所示的顶层模块。

module top(...)

inline u1(

.clk(clk 
),

.a 
(a    ),

.b 
(b    ),

.d1 (in1 
),

.d2 (in2 
),

.d 
(out1 )

);

inline u2(

.clk (clk 
),

.a 
(c    ),

.b 
(d    ),

.d1 (in3 
),

.d2 (in4 
),

.d 
(out2 )

);

endmodule

检验器mutex_chk可以用下面的方式与顶层中内联（inline）的两个模块实例绑定。

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

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

与检验器绑定的设计信号可以包含绑定实例中的任何信号的跨模块引用（cross module reference）