SVA简介

在验证环境中，测试平台承担的三个不同的任务： （1） 产生激励 （2） 自检机制

包括协议检验和数据检验。协议检验的目标是控制信号。数据检验的目的是检验正在处理的数据的完整性。 （3） 衡量功能覆盖

包括协议覆盖和测试计划覆盖。协议覆盖用来衡量一个设计的功能说明书中确定的所有功能是否都测试过。测试计划覆盖用来衡量测试平台的穷尽性。

SVA着重处理在测试平台中被分散在不同部分中讨论的两大类： （1） 协议检验 （2） 协议覆盖

1. SVA定义

断言，又被称为监视器或者检验器。如果一个在模拟中被检查的属性（property）不象我们期望的那样表现，那么这个断言失败。

Verilog也能用来实现一些检查，但相比较而言SVA有如下优点：SVA是一种描述性语言，可以完美的描述时序相关的状况，语言本身非常精确且易于维护 SVA提供若干个内嵌函数来测试特定的设计情况，并且提供了一些构造来自动收集功能覆盖数据。

SVA中定义了两种断言：并发断言和即时断言。

并发断言是基于时钟周期的，在时钟边缘根据调用的变量的采样值计算测试表达式，可以在静态验证和动态验证中使用。

例如：a_cc：assert property(@(posedge clk) not(a && b));

即时断言是基于模拟事件的语义，测试表达式的求值与时序不相关，只可以在动态验证中使用。

例如：always_comb

begin

a_ia：assert (a && b); end

区别并发断言和即时断言的关键词是property。

2.SystemVerilog的调度

在每个time slot，许多事件按照安排的顺序发生。这些事件的列表依照标准定义的算法执行。依照这个算法，模拟器可以防止任何在设计和测试平台互动中的不一致。

图2 SystemVerilog事件进程安排流程表

断言的评估和执行包括以下三个阶段： （1） 预备（Preponed）采样断言变量。

（2） 观察（Observed）对所有的属性表达式求值。

（3） 响应（Reactive）调度评估属性成功或失败的代码。

3.建立SVA块

SVA用关键词sequence（序列）来表示设计中的逻辑事件。序列的基本语法是：

sequence name_of_sequence endsequence

许多序列可以逻辑或者有序的组合起来生成更复杂的序列。SVA提供了一个关键词property（属性）来表示这些复杂的有序行为。属性的基本语法是：

property name_of_property ；or

endproperty

属性必须在模拟过程中被用于断言(assert)、假设(assume)或覆盖(cover)语句来发挥作用。

SVA提供了关键词assert来检查属性。其基本语法是： assertion_name: assert property (property_name);

SVA提供了关键词assume来假设属性。其基本语法是： assertion_name: assume property (property_name);

SVA提供了关键词cover来衡量协议覆盖。其基本语法是： cover_name: cover property (property_name);

上图表明了SVA语言的基本构成。布尔表达式将设计中的信号组合起来，

组成序列。然后序列逻辑或者有序的组合起来得到属性。最后通过关键词assert,cover和assume指示属性的具体作用。

4.SVA序列和属性

4.1简单序列举例

首先以一个只做组合逻辑检查（检查布尔表达式）的序列为例：

sequence s1 @(posedge clk) a; endsequence

序列s1检查信号a在每个时钟上升沿都为高电平。

1clkas12345678 图1 序列s1的波形

从波形图可以看出，一个向上的箭头表示一次成功，一个向下的箭头表示一次失败。并且并行断言使用进程安排中预备（preponed）阶段采样到的值。此例中序列开始时间和结束时间相同。

接下来，介绍一个时序关系的序列： sequence s2

@(posedge clk) a ##2 b; // ##表示时钟周期延迟 endsequence

1clkab2345678s2Attemps ending at time 7 Start time 5 7 Result Success Failure Reason NA a 图2 序列s2的波形

序列s2检查的是如果a在任何一个给定的时钟上升沿为高电平，b应该在两个cycle之后为高电平。与上例中不同的是，序列s2开始时间和结束时间可能不同。

从波形图中可以看出，如果a为低电平，检查失败，s2开始并结束于同一时间。如果a为高电平，序列开始进行时序关系的检查。时序检查的第一个失败开始于2，结束于4；时序检查的第一个成功开始于5，结束于7。注意表示序列成功或失败的箭头都是标注在序列结束的位置。

4.2 蕴含操作符

上一小节中序列s2的失败由两个原因：(1)a为低电平；(2) a为高电平，b在

两个cycle之后不为高电平。通常我们只关心第二种错误，第一种错误是一个无效的错误信息。因而我们希望通过定义某种约束技术，在检查的起始点无效时忽略这次检查。SVA提供了蕴含（Implication）实现这一目的。

蕴含的左边叫做先行算子(antecedent)，右边叫做后续算子 (consequent)。当

先行算子成功时，后续算子才会被计算；如果先行算子不成功，那么整个属性被

默认为“空成功”。另外要注意的是，蕴含只可用于属性定义中，不可用于序列中。

蕴含分为两类：

(1) 交叠蕴含（Overlapped implication）

用符号”|->”表示。如果先行算子匹配，在同一个时钟周期计算后续算子表达式。也可以加入固定延时”|-> ##2”，表示如果先行算子匹配，在两个时钟周期之后计算后续算子表达式。

(2) 非交叠蕴含（Non-overlapped implication）。

用符号”|=>”表示。如果先行算子匹配，在下一个时钟周期计算后续算子表达式。

利用蕴含，序列s2可以改为更符合我们需要的时序检查的属性p3： property p3

@(posedge clk) a |-> ##2 b; // ##表示时钟周期延迟 end property

1clkab2345678p3Attemps ending at time 7 Start time 5 7 Result Success Success Reason NA a 图3 属性p3的波形

从波形图中可以看出，失败只有一个（开始于2，结束于4），真正的成功只

有一个（开始于5，结束于7），其余的成功都为空成功。

4.3 SVA检验器的时序窗口

上面讨论的延迟的例子都是固定的正延迟。延迟也可以用时序窗口的方式定

义，从而给延迟限定一个范围。 例如：

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

上述表达式实际上以下面三个线程展开：

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

时序窗口可以用于属性以及序列。不同的是，第一个成功的线程将使整个属

性成功，并结束这个属性；而序列可以有多个匹配都能使得序列成功，即第一个成功并不结束这个序列的检查，序列可以有多个成功的结束点。

时序窗口左边的值最小为0。时序窗口右边的值最大为$（它指示一个有限的

但无边界的最大值）。检验器不停的检查表达式是否成功直到模拟结束。如果属性检查在模拟结束之前都没有成功，那么检查报告为“未完成的检验（incomplete check）”。如果序列在模拟结束之前检查没有结束，那么检查报告也为未完成的检验。 例如： sequence s4;

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

endsequence property p4;

@(posedge clk) s4; endproperty

1234567101112clkabs4p4图4 序列s4和属性p4的波形

在时钟周期2，开始一次有效的检查。在时钟周期3，出现了第一次成功，

使得这次的p4检查结束，但是s4继续检查，并在时钟周期4检查到第二次成功。在时钟周期11，开始第三次有效的检查，由于模拟结束时，还未满三个周期， 并且b在模拟结束之前都没有成功，因此这次的检验序列s4和属性p4都为incomplete check。

➢ 大的时间窗口应该使用变量予以限定

当##[M:N]和[*M:N]运算符中的时间间隔很长（如大于20个时钟周期）时，编译或运行这样的运算符要占用很长的时间和很多的资源。 例如，带长时间间隔的非重叠事务：

a1:assert property(@(clk)start |-> ##[150:256] stop); 可改写位

logic [10:0] timer=0;

always @(posedge clk) begin:nooverlap if(reset||stop) timer<=0; else if(start) timer<=1;

else if(timer!=0 && timer<=255) timer<= timer + 1;

timing:assert property disable iff(reset)

$rose(stop)||$rose(timer==256) |-> ((timer>150) && (timer<=255)) )else …； end:nooverlap

4.4序列操作符

序列操作符包括重复运算符、延迟运算符、二元运算符等。下表列出一些操作符的优先级和关联性：

4.4.1重复运算符

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

4.4.1.1连续重复

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

基本语法如下：

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

1clkstartastop23456710111213141516a5 图5 属性p5的波形

属性p5检查的是检验有效的开始2个cycle之后，a连续为高3个cycle，再过2个cycle，stop为高一个cycle。

4.4.1.2跟随重复

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

跟随重复的基本语法如下： signal [->n]

4.4.1.3非连续重复

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

非连续重复的基本语法如下： 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

clkstartastopp6p71s1e2s2e3s 图6 属性p6和p7的波形

属性p6和p7做的检查为：在任何时钟上升沿start拉高后开始检查，两个时

钟周期后，信号a连续或者间断的出现3次为高，接着信号stop在下一个时钟周期为高。p6与p7的唯一区别是，p6要求a第三次为高后的那个时钟周期stop必须为高，而p7只要求在a的第三个匹配之后，期望一个有效的信号stop，但不必在下一个时钟周期发生。

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

4.4.2选择运算符

SVA允许在序列和属性中使用选择运算符。 例如 property p8;

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

endproperty

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

4.4.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

123456710clkabcds9cp9 图7 序列s9c和属性p9的波形

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

（2）intersect运算符

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

（3）or运算符

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

4.4.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的第一次匹配。

4.4.5 throughout构造

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

(expression) throughout (sequence definition)

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

4.4.6 within构造

within构造允许在一个序列中定义另一个序列。 其基本语法为： seq1 within seq2

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

不晚于seq1的开始匹配点，seq2的结束匹配点必须不早于seq1的结束匹配点。

4.5 属性操作符

一个属性定义了设计的一个行为。一个属性可以作为一个假设、一个检查器或者一个覆盖率规范被用于验证。为了将这种行为用于验证，必须使用断言(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

在序列、属性中都可以定义时钟。通常情况下， 在属性的定义中指定时钟，

并保持序列于时钟是一种好的编码风格，这样可以提高序列的重用性。

4.6 disable iff

SVA提供了关键词disable iff来实现检验器的复位，即某些条件为真时，我

们不想执行检验。其基本语法如下：

disable iff (expression)

disable iff只可用在属性中。

例如：

property p_dis;

@(posedge clk)

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

1clkreset23456710111213startap_dis 图8 属性p_dis的波形

可以从波形图中看出，在时钟周期13，如果没有reset信号的复位，属性将会失败。但是由于reset信号拉高，未结束的检验就失效，属性得到一个空成功。

4.7系统函数

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)：在任意给定的时钟沿，计算向量中为高的位的数量。

4.8参数

4.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));

4.8.2使用参数的SVA检验器

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

4.9局部变量

在序列或者属性的内部可以局部定义变量。局部变量能够在需要的时候在一

个序列或者属性实例中动态地产生并能在序列结束的时候移除。变量的赋值接着子序列放置，用逗号隔开。

例如：

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

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

任务、任务线程、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\endsequence

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

4.11一个序列结束点的检测和使用

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个时钟周期。

clkabcdp0p1 图9 属性p0和p1的波形

4.12 true表达式

使用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成功匹配点是否相隔一个时钟周期。

4.13 SVA中的多时钟定义

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

4.13.1多时钟序列

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

例如：

sequence s_mul_clk;

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

12134526783910111213141515clk1clk2abs_mul_clkAttemps ending at time 14 Start time 11 12 13 Result Success Success Success Reason NA NA NA 图10 序列s_mul_clk的波形

序列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

4.13.2多时钟属性

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

@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk1) s2 多时钟属性也可以使用逻辑运算符（and,or,not）连接两个单时钟序列。

4.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

12345671011121314151617181920211234567clk1clk2startabcstope1e2 图11 序列e1和e2的波形

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

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

5 SVA检验器

SVA提供了关键词assert来检查属性，assert语句的基本语法是： assertion_name: assert property(property_name);

5.1执行块

执行块可以在属性成功或者失败后执行某些语句。 执行块的基本语法如下： assertion_name:

assert property (property_name) ; else ;

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

5.2 SVA检验器和设计连接

有两种方法可以将SVA检验器连接到设计中： （1） 在模块定义中内建或者内联检验器。

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

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

绑定的语法如下：

bind

;

举例说明绑定的使用： 下面为检验器模块的代码： 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);

6功能覆盖

功能覆盖分为两类：对属性的覆盖和对序列的覆盖。 对属性覆盖的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表示主控设备正在请求总线）。

Req1 0 1 1 0 1 0 0 Req2 1 0 1 0 0 1 0 Req3 1 1 0 1 0 0 0 测试平台应该生成上表中所有的输入组合。

property p_req1;//master 1 requesting @(posedge clk) $fell(req1) && req2 && req3; endproperty c_req1:cover property(p_req1) begin creq1++; if(creq1==3) creq1_flag=1’b1; end c_req2:cover property(p_req2) begin creq2++; if(creq2==3) creq2_flag=1’b1; end property p_req2;//master 2 requesting @(posedge clk) $fell(req2) && req1 && req3; endproperty …… …… property p_req123;//master 1&2&3 requesting @(posedge clk) $fell(req1) && $fell (req2) && $fell (req3); endproperty c_req123:cover property(p_req123) begin creq123++; if(creq123==3) creq123_flag=1’b1; end

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

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

7.assume语句

在形式验证和动态仿真中，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语句不能使用执行块，因为执行语句对于假设来说没有意义。

8.expect构造

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语句检验成功或者失败后才执行。

9.SVA模拟方

当每个设计模块完成后，应该对它们进行彻底的测试。在块的集成前必须发现块内的边缘缺陷（corner case bugs），因为在系统级发现这些缺陷是非常困难的。在模块级，模拟工作量比较少，因此缺陷容易被跟踪并快速修复。

在用SVA进行块级验证中推荐下面的技巧：

(1) 所有为块级设计而写的SVA检验都应该是内嵌的。块级断言经常要访问设计

的内部寄存器，因此把检验内嵌到设计模块更为有效率。

(2) 模块级的SVA检验的引用应该由设计模块内定义的参数来控制。这样就能够

根据模拟的不同需求，自由打开或关闭这些检验。

(3) SVA一共有四个等级的错误严重级别：$fatal（致命错误，将导致模拟结束），

$error，$warning，$info。所有的错误都会打印一个出错信息，但提示的错误级别不同。SVA里默认的严重级别为error。模块级的SVA检验的严重级别应该由设计模块内定义的参数来控制。

module master(…)

parameter a_sva = 1'b1; //控制打开或关掉断言

parameter a_sva_severity = 1'b1; //控制断言的严重级别 always@(posedge clk) begin

if(a_sva) begin

a_comp:assert(p_chk)

else if(a_sva_severity) $fatal; end end …

endmodule

(4) 每个模块级的SVA检验都应该被执行并覆盖到，就是说所有模块级检验一定

要至少有一次真正的成功。

单独的模块验证完成后，需要对整个系统进行验证。 在用SVA进行系统级验证是推荐下面的一些技巧：

(1) 由于单个块的内部功能已经仔细验证过，所以为了提高性能，在默认状态下，

在系统级验证时不要把块级断言包含进去。

(2) 如果性能不是瓶颈，可以在系统级验证中把块级断言包含进去，因为系统接

口提供了更加真实的和一些期望之外的输入情况。 (3) 如果有断言失败，验证环境要提供机制来激活模块级断言。

例如可以在顶层模块中实例化master模块：

master #(.master_sva(1’b1), .master_sva_severity(1’b1)) u1(…);

这样就能够通过传入的参数值，在顶层模块中控制块级断言是否执行。 (4) 在系统级，断言检查更应该关注接口规则而不是块内部细节。

10.数据集约型（data intensive）设计

对于任何设计，有两个方面必须完全验证： 1. 控制逻辑是否正确。

2. 输出的数据是否与预期的一致。

SVA语言特有的描述性使它更适用于时序检验，也就是说适合检验那些有着复杂时序关系的控制逻辑控制信号。虽然断言并没有对数据校验增加额外价值，但它仍可以用于编写有效自检环境。

SVA在数据集约型设计中的优点：

➢ SVA使用SystemVerilog语言自身的大多数数值类型和操作符，这使得它可

以灵活地用于编写简单算术校验。

➢ 通过使用tasks和functions，数据验证可以自动完成。

➢ 动态的数据通路SVA检验器智能的使用时钟周期，无需等到模拟结束就可

以发现设计问题。检验器可以指出错误的确切所在处，从而使查错变得更简单。

10.1数据通路检验的例子

我们通常所做的数据检验是把输出的数据存入一个文件，然后在与黄金模型（Golden Model，通常用C构建）的输出对比。虽然这种方法是可行的，但它有着以下缺点：

(1) 需要在跑完整个模拟后才能与预期结果对比，如果结果出错，则浪费了很多模拟时间。

(2) 这种方法不利于查错，因为它无法显示流水线的哪一阶段开始出错。 更有效的检验数据的方法是动态地进行对比，其动态检验过程如下图所示：

输入数据流水线阶段输出数据流水线阶段的黄金结果通用检验器的对比结果对比结果成功/失败图12 数据通路动态检验

首先用黄金C模型产生流水线各阶段的结果，存入不同的文件中；然后对

RTL使用相同的输入文件来进行数据验证；创建一个检验器来载入黄金结果，然后与RTL模拟动态对比。在模拟进行的同时，当遇到相应的触发点，检验器会对比模拟结果与黄金结果，并且报告出错信息。 SVA检验器如下： module dp_chk(

input logic reset,clk,enable, input logic [15:0] d1,…d); parameter data_file =””; …

//打开黄金数据文件 initial begin

fd=$fopen(data_file,”r”); end

//将RTL数据结果存入本地检验器 always@(*) begin

local_array[0] <=d1; …

local_array[63] <=d; end

//将黄金数据结果存入本地检验器 always@(negedge enable) begin if(reset)

$display(“block number %d\\n”,blk); for(j=0;j<;j++)

fdl=$fscanf(fd,”%x”,pix_in[j]); blk++ end //比较结果

genvar k; generate

for(k=0;k<;k++) begin : loop

a_chk: assert property (@(posedge clk)

(reset && $fell(enable)) |=> (pix_in [k]== local_array [j])) else $fatal; end

endgenerate endmodule

下面是检验器的实例：

bind data_feeder dp_chk #(.data_file(“input_image.dat”))

dpchk1(reset,clk,latch_en,q0,…q63);

bind data_path dp_chk #(.data_file(“xposed.dat”))

dpchk2(reset,clk,dp_en2,dw0,…dw63);

在数据检验的例子中，我们可以发现SVA的如下优点：

➢ 通过一些参数的定义（例如定义黄金数据文件），我们就可以创建一个通用检验器，将其用于检验所有的流水线阶段的结果。通过使用bind语句结构，检验器可与数据通路的特定点相连接。

➢ 由于数据通路一次只检验个数据点，因此我们使用一个变量（blk）递增来记录哪一个数据块正在被处理。

➢ 在数据的比较中，经常会涉及数组的比较。关键词generate能够产生一组属性来验证多个数据点。通过类型genvar定义数据，并使用for循环产生多个不同的属性，每一个属性同时验证一个数据点。 ➢ SVA提供了系统任务$fatal在断言失败时退出模拟。