SystemVerilog -- 11.0 Introduction

SystemVerilog Assertions

系统的行为可以写成一个assertion，该assertion在任何时候都应该为真。因此，assertion用于验证定义为属性的系统的行为，也可用于功能覆盖。

What are properities of a design ?

如果assertion检查的设计属性未按预期方式运行，则assertion将失败。例如，假设设计请求授权，并期望在接下来的四个周期内收到确认。但是，如果设计在第五个周期上获得ack，则应在 4 个时钟内返回 ack 的属性被违反，并且assertion失败。

如果禁止由assertion检查的设计属性发生，则assertion将失败。例如，假设一个小型处理器解码从内存中读取的指令，遇到未知指令并导致致命错误。如果设计中从未预料到这种情况，则会违反只能从内存中读取有效指令的设计属性，并且assertion失败。

从上面的两个示例这可以明显看出，通过编写 SystemVerilog assertion 来检查给定设计的属性。

Why do we need assertions ?

assertion只不过是功能检查器的更简洁的表示。assertion表示的功能也可以编写为涉及更多代码行的SystemVerilog任务或检查器。下面列出了这样做的一些缺点：

• SystemVerilog 冗长且难以维护和扩展属性数量的代码
• 作为一种过程语言，很难编写在同一时间段内设计许多并行事件的检查器

// A property written in Verilog/SystemVerilog
always @(posedge clk) begin
  if (!(a && b))
    $display ("Assertion failed");
end

SystemVerilog assertion 是一种用于指定时态条件的声明性语言，非常简洁且易于维护。

// The property above written in SystemVerilog Assertions syntax
assert property (@(posedge clk) a && b);

Types of Assertion Statements

Assertion语句可以是以下类型：

Building Blocks of Assertions

Sequence

多个逻辑事件的序列通常构成任何设计的功能。这些事件可能跨越多个时钟，也可能只存在于单个时钟周期内。为了简单起见，可以使用简单的assertion来描述较小的事件，然后可以使用这些assertions来构建更复杂的行为模式。

// Sequence syntax
sequence <name_of_sequence>
  <test expression>
endsequence

// Assert the sequence
assert property (<name_of_sequence>);

Property

这些事件可以表示为a，并且可以组合多个序列以创建更复杂的序列或属性。sequence
为了assert它，必须在 or 中包含时钟事件。sequence property

// Property syntax
property (<name_of_property>);
  <test expression> or
  <sequence expressions>
endproperty

// Assert the property
assert property (<name_of_property>);

有两种assertions，Immediate Assertion和Concurrent Assertions。

Immediate Assertion

Immediate Assertion的执行方式与过程块中的语句类似，并遵循模拟事件语义。这些用于在仿真期间验证直接属性。

always @ (<some_event>) begin
  ...
  // This is an immediate assertion executed only at this point in the execution flow
  $assert(!fifo_empty);   // Assert that fifo is not empty at this point
  ...
end

Concurrent Assertions

Concurrent assertions基于时钟语义，并使用其表达式的采样值。使用SystemVerilog属性描述电路行为，该属性每次都会在给定时钟上进行评估，仿真中的故障表明所述功能行为被违反。

// Define a property to specify that an ack should be returned for every grant within 
 1:4 clocks
property p_ack;
  @(posedge clk) gnt ##[1:4] ack;
endproperty  

assert property(p_ack); // Assert the given property is true always

Steps to create assertions

Following are the steps to create assertions:

• Step 1: Create boolean expressions
• Step 2: Create sequence expressions
• Step 3: Create property
• Step 4: Assert property

Example

当a为高电平时，第一个序列s_ab验证b在下一个时钟为高电平，第二个序列s_cd验证d在发现c为高电平后2个时钟为高电平。assert第二个序列位于第一个序列之后的下一个循环中。property

module tb;
  bit a, b, c, d;
  bit clk;

  always #10 clk = ~clk;

  initial begin
    for (int i = 0; i < 20; i++) begin
       {a, b, c, d} = $random;
       $display ("%0t a=%0d b=%0d c=%0d d=%0d", $time, a, b, c, d);
       @(posedge clk);
    end
    #10 $finish;
  end

  sequence s_ab;
    a ##1 b;
  endsequence

  sequence s_cd;
    a ##2 d;
  endsequence

  property p_expr;
    @(posedge clk) s_ab ##1 s_cd;
  endproperty

endmodule

请注意，使用statement assert的属性存在一些冲突。

模拟日志

Compiler version P-2019.06-1；Runtime version P-2019.06-1；Jan 8 05:02 2020
Warning : License for product VCSRuntime_Net(725) will expire within 10 days, on: 17-jan-2020.

If you would like to temporarily disable this message, set the VCS_LIC_EXPIRE_WARNINC environment variable to the number of days before expiration that you want this message to start (the minimum is 0).
0 a=0 b=1 c=0 d=0
10 a=0 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 10ns failed at 10ns 
    Offending 'a'
30 a=1 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 30ns failed at 30ns 
    Offending 'a'
50 a=0 b=0 c=1 d=1
70 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 70ns failed at 70ns 
    Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 50ns failed at 70ns 
    Offending 'b'
90 a=1 b=1 c=0 d=1
110 a=0 b=1 c=0 d=1
130 a=0 b=0 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 130ns failed at 130ns 
    Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 90ns failed at 130ns 
    Offending 'c'
150 a=0 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 150ns failed at 150ns 
    Offending 'a'
170 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 170ns failed at 170ns 
    Offending 'a'
190 a=0 b=1 c=1 d=0
210 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 210ns failed at 210ns 
    Offending 'a'
230 a=1 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 190ns failed at 230ns 
    Offending 'c'
250 a=1 b=1 c=0 d=0
270 a=1 b=0 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 230ns failed at 270ns 
    Offending 'c'
290 a=0 b=1 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 270ns failed at 290ns 
    Offending 'b'
"testbench.sv", 28: tb.unnamed$$_3: started at 250ns failed at 290ns 
    Offending 'c'
310 a=0 b=1 c=0 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 310ns failed at 310ns 
    Offending 'a'
330 a=1 b=0 c=1 d=0
"testbench.sv", 28: tb.unnamed$$_3: started at 330ns failed at 330ns 
    Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 290ns failed at 330ns 
    Offending 'c'
350 a=1 b=1 c=0 d=1
370 a=1 b=1 c=1 d=1
"testbench.sv", 28: tb.unnamed$$_3: started at 370ns failed at 370ns 
    Offending 'a'
"testbench.sv", 28: tb.unnamed$$_3: started at 390ns failed at 390ns 
    Offending 'a'
$finish called from file "testbench.sv", line 13.
$finish at simulation time     400