断言

断言主要用于验证设计的行为。断言是在仿真期间嵌入设计中或绑定到设计单元的检查。当特定条件或事件序列失败时，会生成警告或错误。

“断言中使用的变量值在时间槽的预先区域采样，断言在观察区域进行评估。”

assertion

使用断言的优点

检查设计规范并在失败时报告错误或警告。
改善调试时间。例如，由于非法状态转换引起的错误可能会传播到输出。
可用于形式验证。

序号	断言
1.	立即断言（Immediate assertion）
2.	并发断言（Concurrent assertion）
3.	SVA 构建模块（SVA Building Blocks）
4.	SVA 序列（SVA Sequence）
5.	蕴涵运算符（Implication Operator）
6.	重复运算符（Repetition Operator）
7.	SVA 内置方法（SVA Built in methods）
8.	禁用 iff 和结束（Disable iff & Ended）
9.	SVA 中的变量延迟（Variable delay in SVA）

断言有两种类型：

立即断言（Immediate Assertions）
并发断言（Concurrent Assertions）

立即断言（Immediate Assertion）#

立即断言语句是在过程代码执行时对表达式进行的测试。如果表达式的值为X、Z或0，则解释为假，并且断言失败。否则，表达式解释为真，断言通过。

语法:

label: assert(expression) action_block;

示例:

condition1:assert (A==0 && B==0) $display(" %0t, A=0 and B=0, assertion failed" ,$time);

action_block 在评估断言表达式后立即执行。
action_block 指定在断言成功或失败时采取的操作。

action_block

如果表达式计算结果为真，则执行 pass 语句。
与 else 关联的语句称为 fail 语句，如果表达式计算结果为假，则执行该语句。
pass 和 fail 语句都是可选的。
由于断言是一种必须为真的声明，断言失败将具有相关的严重性。默认情况下，断言失败的严重性为错误。
可以通过在 fail 语句中包含以下严重性系统任务之一来指定其他严重性级别：

$fatal - 生成运行时致命断言错误，终止仿真并返回错误代码。
$error - 是一个简单的 SystemVerilog 构造，发出错误严重性消息。
$warning - 是一个运行时警告，可以以工具特定的方式抑制。
$info - 表示断言失败没有特定的严重性。

如果断言失败且未指定 else 子句，则工具默认调用 $error。

以下是带有和不带可选项的不同形式的立即断言语法：

带有 Pass 和 Fail 语句；Fail 严重性 info

       assert(expression)   
       $display("expression evaluates to true"); 
       else   
       $info("expression evaluates to false");

只有 Pass 语句

       assert(expression)  
       $display("expression evaluates to true");

带有 Pass 和 Fail 语句；Fail 严重性 fatal

       assert(expression) $display("expression evaluates to true");  
       else 
       $fatal("expression evaluates to false");

只有 Fail 语句；Fail 条件中有多个语句且 Fail 严重性为 fatal

       assert(expression)  
       else begin  
        ......
        ......
       $fatal("expression evaluates to false");  
       end

只有 Fail 语句；Fail 严重性为 warning

       assert(expression)  
       else 
       $warning("expression evaluates to false");

带有标签和 Fail 语句；Fail 严重性为 warning

       label: assert(expression)   
       else 
       $warning("expression evaluates to false");

示例:

代码片段

       always @(posedge clk) 
       begin 
       assert (A==0 && B==0) $display("%0t, A=0 and B=0, assertion failed\n",$time);
  
       else assert (A==0 && B==1) $display("%0t, A=0 and B=1, assertion failed\n",$time);
  
       else assert (A==1 && B==0) $display("%0t, A=1 and B=0, assertion failed\n",$time);
  
       else assert (A==1 && B==1) $display("%0t, A=1 and B=1,assertion Success\n",$time);
  
       else $display("%0t fail\n",$time);
       end

下图显示了立即断言的输出

imm_out

图2. 立即断言输出

imme_vcs

在这里有四种条件，即00、01、10、11，当 A 和 B 都为高电平时，条件成功，因此在该条件下断言成功，对于其他条件，视为失败。

并发断言#

检查分布在多个时钟周期上的事件序列的断言称为并发断言。
它们与其他 always 块并行执行，因此称为并发断言。
与立即断言不同，同时断言仅在时钟节拍时进行评估。因此，它是一种基于时钟的评估模型，并且在并发断言中使用的表达式始终与时钟定义相关联。
用于区分立即断言和并发断言的关键字是 “property”。

以下是创建断言的步骤：

SVA 构建模块#

步骤1： 创建布尔表达式
步骤2： 创建序列表达式
步骤3： 创建属性
步骤4： 断言属性

assert steps

1. 布尔表达式

该功能由多个逻辑事件的组合表示。这些事件可以是简单的布尔表达式。

2. 序列

在任何设计模型中，功能由多个逻辑事件的组合表示。
这些事件可以是在相同时钟边沿上计算的简单布尔表达式，也可以是在一段时间内涉及多个时钟周期的事件。
SystemVerilog 断言提供了一个关键字来表示这些事件，称为 “sequence”。
序列的基本语法如下，

语法

sequence name_of_sequence;  
<test expression> 
endsequence

3. 属性

可以逻辑地或按顺序组合多个序列以创建更复杂的序列。
SystemVerilog 断言提供了一个关键字来表示这些复杂的顺序行为，称为 “property”。

语法

property name_of_property;
  <test expression> or  
  <complex sequence expressions>
endproperty

4. 断言

属性是在仿真期间验证的属性。必须断言该属性以在仿真期间生效。SVA 提供了一个关键字，称为 “assert”，用于检查属性。

语法

assertion_ name: assert property( property_name );

示例:

代码片段

       sequence seq;
       @(posedge clk) (A==1 && B==1);
       endsequence

       property ppt;
       seq;
       endproperty

       assert property (ppt) 
       $display(" %0t, A=1 and B=1, assertion success",$time);
       else 
       $display("%0t, A=%0b and B=%0b,assertion failure", $time,A,B);

下图显示了并发断言的输出

con_out

图4. 并发断言输出

con_vcs

在这里有四种条件，即00、01、10、11，当 A 和 B 都为高电平时，条件成功，因此在该条件下，断言成功；对于其他条件，视为失败。

SVA(System Verilog Assertion) Sequence#

表达式在多个时钟周期内扩展称为序列。序列是基于 SystemVerilog 布尔表达式构建的。如果一个表达式检查正确，则序列匹配。这些表达式在一段时间内进行评估，可能涉及一个或多个时钟周期。

一个属性可能涉及检查从不同时间开始的一个或多个顺序行为。对序列的尝试评估是在特定时钟周期开始处搜索序列的匹配。为了确定是否存在这样的匹配，从特定时钟周期开始评估适当的布尔表达式，并在每个连续的时钟周期中继续，直到找到匹配或推断不存在匹配。

语法

     sequence <sequence_name>;
     <test expression>;  
     endsequence

序号	序列
1.	时间关系
2.	逻辑关系
3.	多个序列
4.	形式参数

时间关系
逻辑关系
多个序列
形式参数

1.时间关系序列#

在 SVA 中，时钟周期延迟用 x “##” 符号表示。例如，##5 表示 5 个时钟周期。

语法:

      sequence seq_name;
      变量_1  ##<延迟值>  变量_2 ;
      endsequence

代码片段:

      sequence seqA;
      x ##5 y ;
      endsequence  

      property prop;
      @(posedge clk) seqA;
      endproperty  

     time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

以下序列检查给定正边沿时信号“x”是否为高电平。如果在任何给定的正边沿时信号“x”为高电平，并且 5 个时钟周期后信号“y”应为高电平。如果断言通过，则断言通过，否则断言失败。

2.逻辑关系序列#

语法:

      sequence seq_name;
      变量_1 <逻辑运算符> 变量_2;
      endsequence

代码片段:

      sequence seqB;
      x && y;
      endsequence  

      property prop;
      @(posedge clk) seqB;
      endproperty  
  
      time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

上面的序列 seqB 检查了在时钟的每个正边沿上，信号“X”和“Y”是否都为高电平，如果是，则断言将通过。如果其中一个信号低电平，则断言将失败。

3.多个序列#

多个序列使用运算符、延迟、时钟等进行评估和检查。
下面显示了两个序列 ‘seqA’ 和 ‘seqB’：

代码片段:

      sequence seqA;
      x ##5 y ;
      endsequence  

 
      sequence seqB;
      x && y;
      endsequence  

      property prop;
      @(posedge clk) seqA |-> seqB;
      endproperty     

      time_a1:assert property(prop)  $info("assertion passed");  else $error("assertion failed");

在 seqA 中，x ##5 y 显示 ‘x’ 和 ‘y’ 之间的时间关系，有五个时钟周期。
在 seqB 中，x && y 显示 ‘x’ 和 ‘y’ 之间的逻辑关系，使用逻辑 AND 运算符。
在 property(prop) 内部，我们使用重叠蕴含运算符（|->）来评估这两个序列。
在 seqA 中，如果 x 为高电平，则在 5 个时钟周期后，将评估 y 并且 y 应为高电平。
在 seqB 中，如果 x 和 y 都为高电平，则评估 seqB。
在属性 ‘seqA |-> seqB ’ 中，如果 seqA 为真，则使用重叠蕴含运算符在同一时钟周期评估 seqB。如果为真，则断言通过，否则失败。

输出

下图显示了断言中序列的输出。

vnc seq

波形图

seq vnc wave

解释

在并发断言中，断言仅在时钟上升沿时进行评估。输入条件的影响仅在下一个上升沿时反映出来。输出显示，在 seqA 中，x=1 在 30ns，并且在 5 个时钟周期后，y=1 在 50ns。在 seqB 中，在 50ns 后，x 和 y 都为高电平。在 50ns 到 62ns 之间，断言将通过。

4.带有形式参数的序列#

序列可以具有形式参数，以使序列可重用。形式参数可以用两种类型表示：

带有数据类型的（Typed）
不带数据类型的（Untyped）

代码片段:

       sequence notype_seq (X,Y);
         X && Y;
       endsequence

       sequence withtype_seq (bit X, bit Y);
         X && Y;
       endsequence

       property a_b_notype_prop(a,b);
         @ (posedge clk) a |-> notype_seq(a,b);
       endproperty

       property c_d_type_prop(bit c, bit d);
         @ (posedge clk) c |-> withtype_seq(c,d);
       endproperty

       a_b_notype_assert : assert property (a_b_notype_prop(a,b))
                           $info("assertion passed");
                           else
                             $error("assertion failed");
       c_d_type_assert   : assert property (c_d_type_prop(c,d))
                           $info("assertion passed");
                           else
                             $error("assertion failed");

解释

SV 断言中的形式参数示例如上所示。在序列 1 中使用不带类型的形式参数，它们是没有数据类型声明的变量。在序列 2 中，使用带有类型的形式参数包括具有数据类型的变量，例如：(bit X, bit Y)。使用重叠蕴含运算符，两个属性块在初始条件下工作。使用 assert property 评估了输入条件。
在 assertion_1 和 assertion_2 中，如果两个参数都为 1，则断言通过，否则失败，因为在两个序列中我们执行了 And 运算。
在 a_b_notype_property 中，如果 a=1，在 c_d_type_property 中如果 c=1，则检查 notype 序列和 withtype 序列。

输出

formal_argument

波形图

wave_formal_argument

解释

在 25ns 时，a=1，因此它将检查 notype_seq，并且在那里 a=1 且 b=0，因此在 25ns 时 a_b_notype_assert 失败，c=0，因此它不会检查 withtype_seq。
在 35ns 时，a=1，因此它将检查 notype_seq，并且在那里 a=1 且 b=1，因此在 35ns 时 a_b_notype_assert 通过，c=1，因此它将检查 nontype_seq 并且在那里 c=1 且 d=1，因此在 35ns 时 c_d_type_assert 通过
在 45ns 时，a=1，因此它将检查 notype_seq，并且在那里 a=1 且 b=0，因此在 45ns 时 a_b_notype_assert 失败，c=1，因此它将检查 nontype_seq 并且在那里 c=1 且 d=1，因此在 45ns 时 c_d_type_assert 通过
在 55ns 时，a=1，因此它将检查 notype_seq，并且在那里 a=1 且 b=1，因此在 55ns 时 a_b_notype_assert 通过，c=1，因此它将检查 nontype_seq 并且在那里 c=1 且 d=0，因此在 55ns 时 c_d_type_assert 失败

序列中的可变延迟#

静态延迟

静态延迟意味着在序列内部使用 ’ ## ’ 运算符。这与具有时间关系的序列相同。

语法:

variable_1  ## delay_value  variable_2;

示例:

a ##5 b;

可变延迟

可变延迟类似于循环。这是静态延迟的主要优势。

     parameter_delay = 2;
    
     sequence delay_sequence(variable_delay);
     int delay;
     (1,delay=variable_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);
     endsequence
     
     a_1: assert property(@(posedge clk) a |-> delay_sequence(parameter_delay) |-> b)
     $info("assertion passed"); else $error("assertion failed");

解释

上面的程序显示了断言中可变延迟的示例。在程序内部，我们将参数延迟分配为 ‘2’。此 parameter_delay 被复制到 variable_delay，变量值将在每个时钟周期减少，并检查 ‘delay’ 的值是否等于 ‘0’。序列 delay_sequence 具有一个可变 parameter_delay，该参数从属性传递。实际上被分配给局部变量 delay 的是 variable_delay。
‘*0’ 称为空匹配。例如 a[*0:$] |-> b 意味着 a [*0] 或 a [*1] 或 a [*2] .. a [$]
为了避免由于多次匹配而导致的意外行为，或者导致断言永远不会成功，因为必须测试所有前提线程以使属性成功。‘first_match’ 运算符仅匹配评估尝试的第一个可能的多个匹配，并导致丢弃所有后续的匹配。

输出

variable vnc wave

波形图

参数延迟为 -2 variable correct vncwave

解释

输出显示，在程序内部，我们将参数延迟分配为 ‘2’。首先在 5ns 时取 a=1，在经过 2 个时钟周期后，即在 15ns 时，b 不为高电平。因此，断言失败。在 15ns 到 25ns 之间，a 和 b 是相同的，断言不会被采用，因为 ‘first match’ 避免了重复。在 25ns 到 35ns 之间，输入 a 和 b 的效果为高电平，因此将通过断言。此外，在 45ns 到 55ns 之间，断言被通过。

蕴含运算符#

如果我们希望仅在 “a” 高电平之后检查序列，可以通过使用蕴含运算符来实现。蕴含等价于一个 if-then 结构。
蕴含的左侧称为“前提”，右侧称为“结果”。
它只能用于属性定义，不能用于序列。
有两种类型的蕴含运算符：
1. 重叠蕴含（|->）
2. 非重叠蕴含（|=>）

1. 重叠蕴含#

用 |-> 表示。
如果前提匹配，则结果表达式将在 同一个时钟周期 中计算。

语法：-

<前提> |-> <结果>

例子：-

    property p;
       @(posedge clk) a |-> b;
    endproperty  
    a: assert property(p);

在上述示例中，当在时钟周期的上升沿时，“a”为高电平，则将评估“b”，并基于此进行断言是否通过或失败。

代码片段：

      module overlapped_assertion;
      bit clk,a,b,valid;
  
      always #5 clk = ~clk; //clock generation
  
      //generating 'a'
      initial begin
        valid=1; a=1; b=1;
       #15 a=1; b=0;
       #10 b=1;
       #12 b=0;
       #10 a=0; b=1;
        valid=0;
       #15 a=1; b=0;
       #100 $finish;
      end
     
      // property definition
      property p;
        @(posedge clk) valid |-> (a ##3 b);
      endproperty
 
     //calling assert property
       a_1: assert property(p)
         $info("pass");
         else
          $info("fail");
 
     endmodule

输出：

下图显示了重叠蕴含的输出。在这里，5ns时出现第一个posedge，此时valid和a均为高电平，因此在35ns时将检查b是否高电平，如果此时b不为高电平，则断言失败，此后将遵循相同的过程，直到调用 $finish。

overlapped

输出波形：

overlapped_synopsys

Github实验室代码链接： https://github.com/mbits-mirafra/SystemVerilogCourse/tree/production/assertion/implication_operator/overlapped_implication

Github实验室输出链接： https://github.com/mbits-mirafra/SystemVerilogCourse/blob/production/assertion/implication_operator/overlapped_implication/overlapped.log

重叠蕴含类型：#

结果上带有固定延迟的蕴含#

以下属性检查，如果在给定的正时钟沿上，“a”信号高电平，则2个时钟周期后“b”信号应为高电平。
固定延迟可以表示为 ##n，这里的 n 将指定时间。

语法：-

<前提> |-> ##<value> <结果>

例子：-

property p;  
@(posedge clk) a |-> ##2 b;  
endproperty 
a: assert property(p);

固定延迟

带有序列作为前提的蕴含#

以下属性检查，如果序列 seq_1 在给定的正时钟沿上为真，则开始检查 seq_2（“d”应在 seq_1 为真后的2个时钟周期内为低电平）。

语法：-

<Sequence1> |-> <Sequence2>

例子：-

sequence seq_1;  
(a && b) ##1 c; 
endsequence 

sequence seq_2; 
##2 !d;  
endsequence

property p; 
@(posedge clk) seq_1 |-> seq_2; 
endpeoperty
a: assert property(p);

SVA检查器中的时序窗口#

以下属性检查，如果在给定的正时钟沿上，“a”信号为高电平，则在1到3个时钟周期内，“b”信号应为高电平。

语法：-

<前提> |-> ##[1:<value>] <结果>

例子：-

property p;
@(posedge clk)
a |-> ##[1:3] b; 
endproperty 
a: assert property(p);

时序窗口

重叠的时间窗口#

以下属性检查，如果在给定的正时钟沿上，“a”信号为高电平，则在同一时钟周期内或在4个时钟周期内，“b”信号应为高电平。

语法：-

<前提> |-> ##[0:<value>] <结果>

例子：-

property p;
@(posedge clk)
a |-> ##[0:3] b;
endproperty
a: assert property(p);

重叠的时间窗口

不定时窗口#

右侧指定的时间窗口的上限可以用“$”符号定义，这意味着时间上没有上限。这被称为“事件性”运算符。检查器将持续检查匹配，直到仿真结束。
以下属性检查，如果在给定的正时钟沿上，“a”信号为高电平，则从下一个时钟周期开始，“b”信号最终将变为高电平。

语法：-

<前提> |-> ##[1:$] <结果>

例子：-

property p;
@(posedge clk)
a |-> ##[1:$] b;
endproperty
a: assert property(p);

不定时窗口

2. 非重叠蕴含：#

非重叠蕴含由符号 |=> 表示。
如果前提匹配，则结果表达式将在下一个时钟周期中计算。

语法：-

<前提> |=> <结果>

例子：-

property p;
@(posedge clk) a |=>b;
endproperty
a: assert property( p );

在上面的例子中，如果在给定的正时钟沿上信号“a”为高电平，则信号“b”应在下一个时钟沿上为高电平。

NOI

代码片段：

      module nonoverlapped_assertion;
      bit clk,a,b,valid;
  
      always #5 clk = ~clk; //clock generation
  
      //generating 'a'
      initial begin
        valid=1; a=1; b=1;
       #15 a=1; b=0;
       #10 b=1;
       #12 b=0;
       #10 a=0; b=1;
        valid=0;
       #15 a=1; b=0;
       #100 $finish;
      end
     
      // property definition
      property p;
        @(posedge clk) valid |=> (a ##3 b);
      endproperty
 
     //calling assert property
       a_1: assert property(p)
         $info("pass");
         else
          $info("fail");
 
     endmodule

输出：

下图显示了非重叠蕴含的输出。在这里，5ns时出现第一个posedge，此时valid为高电平，15ns时a为高电平，所以将在45ns时检查b是否为高电平，如果此时b为高电平，则断言通过，如果为低电平，则断言失败，此后将遵循相同的过程，直到调用 $finish。

nonoverlapped

输出波形：

nonoverlapped_synopsys

重复运算符:#

repetition

                               图.23 重复运算符的类型

连续重复#

property p;
@(posedge clk) a |-> ##1 b ##1 b ##1 b;
endproperty 
a: assert property(p);

上述属性检查，如果在给定时钟的 posedge 上，信号“a”为高电平，则信号“b”应连续保持高电平 3 个时钟周期。

连续重复运算符用于指定一个信号或序列在指定数量的时钟周期内连续匹配。

语法:

signal [*n] 或 sequence [*n]

“n” 是重复次数。

使用重复运算符，上述序列可以重写为，

property p;  
@(posedge clk) a |-> ##1 b[*3] ##1 c;  
endproperty 

a: assert property(p);

示例:

    module consecutive_repetition;     
      bit clk,a,b;   
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0;  //15  
       #10 a=0; b=1;  //25  
       #10 a=0; b=1;  //35  
       #10 a=0; b=1;  //45  
       #10 a=1; b=1;  //55  
       #10 a=0; b=1;  //65  
       #10 a=0; b=1;  //75  
       #10 a=0; b=0;  //85  
       #10 a=1; b=0;  //95  
       #10 a=0; b=0;  //105  
       #10 a=1; b=1;  //115  
       #10 a=0; b=1;  //125  
       #10 a=0; b=1;  //135  
       #10 a=0; b=0;  //145  
       #10 a=0; b=0;  //155  
       #10;  
       $finish;  
     end  
   
     //property definition  
     property p;  
       @(posedge clk) a |-> ##1 b[*3];  
     endproperty  

     //calling assert property  
     a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
   
    endmodule

输出:

在下图中，25 纳秒时，a=1，经过 1 个时钟周期（##1）后，b 在连续 3 个时钟周期内均为 1。因此，在 55 纳秒时，$info 显示为通过。在 65 纳秒时，a=1，但经过 1 个时钟周期后，b 仅连续出现 2 次为 1。因此，在 95 纳秒时，$info 显示为失败。在 105 纳秒时，a=1，但经过 1 个时钟周期后，b 变为 0。因此，在 115 纳秒时，$info 显示为通过。

con

波形输出:

con

跟随重复#

跟随重复运算符用于指定一个信号将匹配指定次数，但不一定在连续的时钟周期内。

语法:

signal [->n]

property p;  
  @(posedge clk) a |-> ##1 b[->3] ##1 c;  
endproperty 

a: assert property(p);

上述属性检查，如果在给定时钟的 posedge 上，信号“a”为高电平，则信号“b”应连续保持高电平 3 个时钟周期，随后在“b”第三次为高电平时，“c”应在“b”为高电平后出现高电平。

示例：

    module goto_repetition;  
     bit clk,a,b,c;   
 
     always #5 clk = ~clk; //clock generation  
   
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0; c=0; //15  
       #10 a=0; b=1; c=0; //25  
       #10 a=0; b=1; c=0; //35  
       #10 a=0; b=0; c=0; //45  
       #10 a=0; b=1; c=0; //55  
       #10 a=0; b=0; c=0; //65  
       #10 a=0; b=0; c=0; //75  
       #10 a=1; b=0; c=0; //85  
       #10 a=0; b=1; c=0; //95  
       #10 a=0; b=0; c=0; //105  
       #10 a=0; b=1; c=0; //115  
       #10 a=0; b=0; c=0; //125  
       #10 a=0; b=1; c=0; //135  
       #10 a=0; b=0; c=1; //145  
       #10 a=0; b=0; c=0; //155  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> b[->3] ##1 c;  
     endproperty  
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  

     endmodule

输出:

在下图中，25 纳秒时，a=1，b 可以在任何时钟周期内连续 3 次为 1，不一定是连续的时钟周期，随后 c=1 在 b 后经过 1 个时钟周期后出现高电平，但在 75 纳秒时 c=0。因此，在 75 纳秒时，$info 显示为失败。在 95 纳秒时，a=1，b 连续为 1 3 次，然后在经过 1 个时钟周期（##1）后，即在 155 纳秒时，c=1。因此，在 155 纳秒时，$info 显示为通过。

goto

波形输出:

goto

非连续重复#

这与“转到”重复非常相似，只是它不要求信号重复的最后一次匹配发生在整个序列匹配结束之前的时钟周期内。

语法:

signal [=n]

在“转到”和“非连续”重复中，只允许表达式重复。不允许序列重复。

示例：

    module nonconsecutive_repetition;  
     bit clk,a,b,c;   
 
     always #5 clk = ~clk; //clock generation  
   
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0; c=0; //15  
       #10 a=0; b=1; c=0; //25  
       #10 a=0; b=1; c=0; //35  
       #10 a=0; b=0; c=0; //45  
       #10 a=0; b=1; c=0; //55  
       #10 a=0; b=0; c=0; //65  
       #10 a=0; b=0; c=1; //75  
       #10 a=0; b=0; c=0; //85  
       #10 a=1; b=1; c=0; //95  
       #10 a=0; b=0; c=0; //105  
       #10 a=0; b=1; c=0; //115  
       #10 a=0; b=0; c=0; //125  
       #10 a=0; b=1; c=0; //135  
       #10 a=0; b=0; c=1; //145  
       #10 a=0; b=0; c=0; //155  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> b[=3] ##1 c;  
     endproperty  
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  

     endmodule

输出:

在下图中，25 纳秒时，a=1，b 在 65 纳秒时第三次为 1（不一定在连续的时钟周期内），且经过 1 个时钟周期（##1）延迟后，c 可以在任何时钟周期内为 1。因此，在 85 纳秒时，$info 显示为通过。在 105 纳秒时，a=1，b 在 145 纳秒时第三次为 1，且在 155 纳秒时 c=1。因此，在 155 纳秒时，$info 显示为通过。

noncon

波形输出:

noncon

SVA 函数#

sva_method

$rose#

语法:

$rose(布尔表达式或信号名称)

如果表达式的最低有效位变为 1，则返回 true。否则，返回 false。

property p;    
@(posedge clk) $rose(a)  
endproperty

属性 p 检查信号“a”在每个时钟的上升沿过渡到值 1。如果过渡未发生，则断言将失败。

示例：

    module rose;  
     bit clk,a,b;    
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin  
       a=0; b=0;  
       #15 a=1; b=0;  //15  
       #10 a=0; b=0;  //25  
       #10 a=1; b=1;  //35  
       #10 a=0; b=0;  //45  
       #10 a=1; b=1;  //55  
       #10 a=0; b=0;  //65  
       #10 a=1; b=1;  //75  
       #10 a=1; b=1;  //85  
       #10 a=1; b=0;  //95  
       #10 a=0; b=0;  //105  
       #10 a=1; b=0;  //115  
       #10 a=0; b=0;  //125  
       #10 a=1; b=0;  //135  
       #10 a=1; b=0;  //145  
       #10;  
       $finish;  
     end  
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $rose(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出:

在下图中，25 纳秒时，a=1，但 b=0，因为它之前也是 0。因此，在 25 纳秒时，$info 显示为失败。在 45 纳秒时，a=1，且 b 发生了从 0 到 1 的过渡（之前的 b 在 35 纳秒时为 0，它将检查上一个周期）。因此，在 45 纳秒时，$info 显示为通过。在 65 纳秒时，a=1，且 b 发生了从 0 到 1 的过渡（之前的 b 在 55 纳秒时为 0）。因此，在 65 纳秒时，$info 显示为通过。在 95 纳秒时，a=1，但 b 保持 1，没有发生过渡。因此，在 95 纳秒时，$info 显示为失败。

rose

波形输出:

rose

$fell#

语法:

$fell(布尔表达式或信号名称)

如果表达式的最低有效位变为 0，则返回 true。否则，返回 false。

property p;
  @(posedge clk) $fell(a);  
endproperty

属性 p 检查信号“a”在每个时钟的上升沿过渡到值 0。如果过渡未发生，则断言将失败。

示例：

    module fell;  
     bit clk,a,b;   
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=0;  //15
       #10 a=0; b=1;  //25
       #10 a=1; b=0;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=0;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=0;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $fell(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出:

在下图中，25 纳秒时，a=1，但 b=0，它保持不变（检查上一个周期，15 纳秒时 b=0），没有发生过渡。因此，在 25 纳秒时，$info 显示为失败。在 45 纳秒时，a=1，且 b 从 1 变为 0 过渡（之前的 b 在 35 纳秒时为 1）。因此，在 45 纳秒时，$info 显示为通过。

fell

波形输出:

fell

$stable#

语法:

$stable(布尔表达式或信号名称)

如果表达式的值没有改变，则返回 true。否则，返回 false。

property p;    
  @(posedge clk) $stable(a);   
endproperty

属性 p 检查信号“a”在每个时钟的上升沿上是否稳定。如果发生任何过渡，则断言将失败。

示例：

    module stable;  
     bit clk,a,b;    
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=0;  //15
       #10 a=0; b=0;  //25
       #10 a=1; b=1;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=1;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=1;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $stable(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出:

在下图中，25 纳秒时，a=1，且 b=0，与上一个周期相同，它是稳定的。因此，在 25 纳秒时，$info 显示为通过。在 45 纳秒时，a=1，但 b 从 0 变为 1。因此，在 45 纳秒时，$info 显示为失败。

stable

波形输出:

stable

$past#

语法:

$past(信号名称, 时钟周期数)

提供信号在前一个时钟周期的值。

以下属性检查，在给定的上升沿时钟中，如果“b”为高电平，则 2 个时钟周期之前，a 也为高电平。

property p;   
  @(posedge clk) b |-> ($past(a,2) == 1);  
endproperty 
a: assert property(p);

示例：

    module past;  
     bit clk,a,b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=0;
       #15 a=1; b=1;  //15
       #10 a=0; b=0;  //25
       #10 a=1; b=1;  //35
       #10 a=0; b=0;  //45
       #10 a=1; b=1;  //55
       #10 a=0; b=0;  //65
       #10 a=1; b=1;  //75
       #10 a=1; b=1;  //85
       #10 a=1; b=0;  //95
       #10 a=0; b=0;  //105
       #10 a=1; b=0;  //115
       #10 a=0; b=0;  //125
       #10 a=1; b=0;  //135
       #10 a=1; b=0;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> ($past(b,2) == 1);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出:

在下图中，25 纳秒时，a=1，但在 2 个时钟周期之前的 45 纳秒时，b 不为 1。因此，在 25 纳秒时，$info 显示为失败。在 45 纳秒时，a=1，且在 2 个时钟周期之前的 25 纳秒时，b=1。因此，在 45 纳秒时，$info 显示为通过。

past

波形输出:

past

内置系统函数#

$onehot(expression)#

检查在任何给定的时钟边沿上，表达式只能有一个位为高电平。

语法:

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

断言语句 a_1 检查位向量“state”是否为 one-hot。

示例：

    module onehot;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b00100;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b01000;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10000;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'b11000;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'b01100;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b00000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $onehot(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出:

在下图中，25 纳秒时，a=1，且 b 只有一个位为高电平（即 b=00100）。因此，在 25 纳秒时，$info 显示为通过。在 85 纳秒时，a=1，但 b 有两个位为高电平（即 b=11000）。因此，在 85 纳秒时，$info 显示为失败。

onehot

波形输出:

onehot

$onehot0(expression)#

检查在任何给定的时钟边沿上，表达式只能有一个位为高电平，或者没有位为高电平。

语法:

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

断言语句 a_1 检查位向量“state”是否为零 one-hot。

示例：

    module onehot0;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b00100;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b01000;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10000;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'b11000;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'b01100;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b00000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $onehot0(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出：

在下图中，a 在 25ns 时为 1，并且 b 只有一位为高电平（这在 $onehot0 中是允许的）。因此，$info 在 25ns 时显示通过（Pass）。在 85ns 时，a 为 1，但 b 有两位为高电平，即 b=11000（这在 $onehot0 中是不允许的）。因此，$info 在 85ns 时显示失败（Fail）。

onehot0

波形输出：

onehot0

$isunknown(expression)#

检查表达式的任意位是否为 X 或 Z。

语法:

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

断言语句 a_1 检查向量 “bus” 的任意位是否为 X 或 Z。

示例：

    module isunknown;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b001x0;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b010z0;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10xz0;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'bxxxxx;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'bzzzzz;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b10100;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b10000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> $isunknown(b);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出：

在下图中，a 在 25ns 时为 1，且 b 的一位为未知（即 1x0）。因此，$info 在 25ns 时显示通过（Pass）。在 125ns 时，a 为 1，但 b 的位没有未知（即 10100）。因此，$info 在 125ns 时显示失败（Fail）。

isunknown

波形输出：

isunknown

$countones(expression)#

计算向量中高电平的位数。

语法:

a_1: assert property( @(posedge clk) $countones(bus) > 1 );

断言语句 a_1 检查向量 “bus” 中的高电平位数是否大于 1。

示例：

    module countones;  
     bit clk,a;  
     logic [4:0] b;  
 
     always #5 clk = ~clk; //clock generation  
 
     initial begin
           a=0; b=5'b00000;
       #15 a=1; b=5'b001x0;  //15
       #10 a=0; b=5'b01000;  //25
       #10 a=1; b=5'b11011;  //35
       #10 a=0; b=5'b01000;  //45
       #10 a=1; b=5'b10xz0;  //55
       #10 a=0; b=5'b10000;  //65
       #10 a=1; b=5'bxxxxx;  //75
       #10 a=0; b=5'b01100;  //85
       #10 a=1; b=5'bzzzzz;  //95
       #10 a=0; b=5'b01000;  //105
       #10 a=1; b=5'b11110;  //115
       #10 a=0; b=5'b01000;  //125
       #10 a=1; b=5'b10000;  //135
       #10 a=1; b=5'b00100;  //145
       #10;
       $finish;
     end
 
     //property definition  
     property p;  
       @(posedge clk) a |-> ($countones(b) == 1);  
     endproperty  
     
     //calling assert property  
       a_1: assert property(p)  
           $info("Pass");  
         else  
           $info("Fail");  
 
     endmodule

输出：

在下图中，a 在 25ns 时为 1，并且 b 的一位为 1（即 1x0）。因此，$info 在 25ns 时显示通过（Pass）。在 125ns 时，a 为 1，并且 b 有多位为 1（即 11110）。因此，$info 在 125ns 时显示失败（Fail）。

countones

波形输出：

countones

Disable iff#

在某些设计条件下，如果某个条件为真，我们不希望继续进行检查。这可以通过使用 disable iff 来实现。Disable iff 在检查的表达式有效时禁用该属性。通常用于复位检查，当复位有效时，属性被禁用。下面的属性（property(p)）检查，如果复位无效且信号 “a” 和 “b” 在给定时钟的上升沿为高电平时，属性被断言。在整个序列期间，如果在任何时候检测到复位为高电平，检查器将停止，属性被取消断言。

语法：

property p; 
 @(posedge clk) 
  disable iff (condition); 
endproperty`

示例：

    property p;  
    @(posedge clk)  
    disable iff (reset) (a&&b);  
    endproperty

上面的例子我们使用reset作为检查器。disable iff 仅在属性内部使用。如果复位被取消断言，即“0”，则启用该属性，并获得断言输出。如果复位被置位，则该属性被禁用，则无法获取/显示断言输出。

代码片段

      //Design module
       module andgate(  
        input A,  
        input B,  
       output Y,  
       input clk,  
       input rst);  
      assign Y = A&&B;  
      endmodule:andgate

Testbench 代码:

     `//module AND_gate_tb;
       module AND_Gate;
         reg A;
         reg B;
         reg clk;
         wire Y;
         reg rst;

        //Design instantiation
        andgate inst(.A(A), .B(B), .Y(Y), .clk(clk), .rst(rst));

        always #5 clk = ~clk;
        initial
        begin
        rst <=1; //reset is asserted
        clk<=1;
        A<=0;
        B<=0;

        #10
       A<=0;
       B<=1;
 
 
       #12
       rst <=0;//reset is deasserted
       A<=1;
       B<=0;

       #10
        A<=1;
        B<=1;

       #30 $finish;
        end
      //-------------------------------------------------------
      // Disable iff is used to disable the property when the
      // reset is active. Assertion output is disable whether it
      // failure or pass.It is used when we don't want to check 
      // some conditions
      //-------------------------------------------------------
      property p;
      @(posedge clk) disable iff(rst)//disable if reset is assereted
      A&&B;
       endproperty

      assert property (p) $display("time=%0t,A=%0b and B=%0b, assertion success\n",$time,A,B);
      else $display("time=%0t, A=%0b and B=%0b,assertion failure\n", $time,A,B);
      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:AND_Gate

输出：

在下图中，复位是一个检查器，如果 rst=0，则属性被启用并给出断言输出，而在 40ns 时 rst=1，则属性被禁用，断言输出不被检查。当我们不想检查断言的某些输出时，使用 disable iff。

disablechanged

disablegraph

ended#

关键字 “ended” 被附加到序列名称上，当在程序中使用多个序列时，序列的结束点可以用作同步点。

在下面的代码片段中，我们使用了两个序列 seq1 和 seq2。序列一使用变量 d，序列二使用变量 ‘k’。这两个序列在属性中使用了隐含操作符，以及 4 个时钟周期的延迟。现在，通过使用 “ended” 关键字与序列，例如：seq1 -> ##4 seq2。seq1 是前件，seq2 是后件。如果前件执行，即 seq1。那么只有在执行后件，即 seq2 时才会执行。在代码中，seq1 变量 ’d’ 在时钟上升沿时为高电平，然后从下一个时钟上升沿开始评估 seq2，然后在 4 个时钟周期的延迟后，如果 ‘k’ 为断言则通过。

代码片段

      `module assertion_ex;
       bit clk,d,k;

       always #5 clk = ~clk; //clock generation

      //generating 'a'
      initial
      begin
      d=1;
      #57  k=1;
      #10 d=0;
      #15 k=0;
      #10 d=1;
      #10 k=0;
      #10 d=1;
      #10 k=1;
      #200;
      $finish;
      end

      //sequence 1
      sequence seq_1;
      @(posedge clk)
       d;
      endsequence
  
     //sequence 2
     sequence seq_2;
      @(posedge clk)
      ##4 k;
      endsequence

     property p;
     @(posedge clk) seq_1.ended |-> ##4 seq_2.ended;
    endproperty

    a_1: assert property(p)$info("passed");
    else $info("failed");

      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:assertion_ex

输出：

在这里，在 5 纳秒时，d=1，seq1 从下一个周期开始执行，seq2 开始执行，它将从 seq1 结束周期的下一个周期开始检查 4 个周期。在这里，seq2 检查值 ‘k’ 直到 45 纳秒，在 45 纳秒时，‘k’ 的值为低，然后断言失败。在 25 纳秒时，seq1 的变量 ’d’ 值为 ‘高’，然后它将从下一个周期开始执行 seq2，seq2 的变量 k 将检查 4 个周期内 ‘k’ 是否为高电平。在第 4 个时钟周期中 ‘k’ 为高电平，所以在 65 纳秒时，断言通过。

ended

波形图输出

endedwaveform

不使用 ended 关键字：在这个例子中，不使用 ended。在下面的相同代码中，断言将在 125ns 后通过。变量 seq 的值在 45ns 时为高电平，然后由于 ##4 的延迟，seq2 在经过 4 个时钟周期后进行评估。变量 k 随后被评估，作为表达式 ##4 k；如果在 4 个时钟周期内 ‘k’ 的值为高电平，则断言通过。在这种情况下，需要 9 个时钟周期才能通过断言，而使用 ended 关键字，则断言在 5 个时钟周期内通过。

代码片段

      `module assertion_ex;
       bit clk,d,k;

       always #5 clk = ~clk; //clock generation

      //generating 'a'
      initial
      begin
      d=1;
      #57  k=1;
      #10 d=0;
      #15 k=0;
      #10 d=1;
      #10 k=0;
      #10 d=1;
      #10 k=1;
      #200;
      $finish;
      end

      //sequence 1
      sequence seq_1;
      @(posedge clk)
       d;
      endsequence
  
     //sequence 2
     sequence seq_2;
      @(posedge clk)
      ##4 k;
      endsequence

     property p;
     @(posedge clk) seq_1 |-> ##4 seq_2;
    endproperty

    a_1: assert property(p)$info("passed");
    else $info("failed");

      initial
      begin
      $dumpfile("waveform.vcd");
      $dumpvars();
      end
      endmodule:assertion_ex

输出：

这里，在 45ns 时，d=1，作为变量 ’d’ 的 seq1 在 45ns 时为高电平，然后执行 seq1，接着 seq2 将开始执行变量 ‘k’，在 4 个时钟周期后，它将开始检查 ‘k’ 的值，在 seq2 的第 4 个时钟周期后，seq2 变量 ‘k’ 将检查值。如果它是高电平，则通过断言。总共需要 9 个时钟周期来执行 seq2 的值，在 125ns 时它将通过断言。

without_endedif

输出波形：

without_ended_waveform

立即断言（Immediate Assertion）#

并发断言#

SVA 构建模块#

SVA(System Verilog Assertion) Sequence#

1.时间关系序列#

2.逻辑关系序列#

3.多个序列#

4.带有形式参数的序列#

序列中的可变延迟#

蕴含运算符#

1. 重叠蕴含#

重叠蕴含类型：#

结果上带有固定延迟的蕴含#

带有序列作为前提的蕴含#

SVA检查器中的时序窗口#

重叠的时间窗口#

不定时窗口#

2. 非重叠蕴含：#

重复运算符:#

连续重复#

跟随重复#

非连续重复#

SVA 函数#

$rose#

$fell#

$stable#

$past#

内置系统函数#

$onehot(expression)#

$onehot0(expression)#

$isunknown(expression)#

$countones(expression)#

Disable iff#

ended#

On this page:

Tags