SystemVerilog -- 11.2 SystemVerilog Concurrent Assertions

SystemVerilog Concurrent Assertions

Concurrent Assertions描述了跨越仿真时间的行为，并且仅在时钟边沿发生时进行评估。

SystemVerilog Concurrent Assertions语句可以在与其它语句同时运行的模块、接口或程序块中指定。以下是Concurrent Assertions的属性：

• 根据采样变量中的值在时钟边沿评估测试表达式
• 变量的采样是在预设区域完成的，表达式的评估是在仿真调度器的观察区域完成的
• 它可以放置在过程、模块、接口或程序块中
• 它可用于动态和形式验证技术

Example #1

两个信号a和b在适中的正边沿声明和驱动，并具有一些随机值，以说明Concurrent Assertions的工作原理。Assertions由Immediate语句编写，该语句定义了时钟事件中信号之间的关系。assert property

在本例中，在整个仿真中，信号a和b在时钟的正沿均应为高电平。对于发现a或b为零的所有实例，Assertion预计会失败。

module tb;
  bit a, b;
  bit clk;

  always #10 clk = ~clk;

  initial begin
    for (int i = 0; i < 10; i++) begin
      @(posedge clk);
      a <= $ramdom;
      b <= $ramdom;
      $display ("[%0t] a=%0b b=%0b", $time, a, b);
    end
    #10 $finish;
  end

  // This assertion runs for entire duration of simulation
  // Ensure that both signals are high at posedge clk
  assert proerty (@(posedge clk) a & b);
endmodule

Assertion在clk的每个正边沿上执行，并使用预置区域中的变量值计算表达式，这是给定时钟边沿之前的增量周期。因此，如果时钟从0变为1的同一边沿上的a从0变为1，则用于Assertion的a的值将为零，因为它在时钟边沿之前为零。

可以看出，对于发现a或b为零的所有情况，assertion都失败，因为语句中给出的表达式在整个模拟过程中都应为真。assert

模拟日志

Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 15:26 2019
[10] a=0 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 10ns failed at 10ns
  Offending '(a & b)'
[30] a=0 b=1
"testbench.sv", 24; tb.unnamed$$_4: started at 30ns failed at 30ns
  Offending '(a & b)'
[50] a=1 b=1
[70] a=1 b=1
[90] a=1 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 90ns failed at 90ns
  Offending '(a & b)'
[110] a=1 b=1
[130] a=0 b=1
"testbench.sv", 24; tb.unnamed$$_4: started at 130ns failed at 130ns
  Offending '(a & b)'
[150] a=1 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 150ns failed at 150ns
  Offending '(a & b)'
[170] a=1 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 170ns failed at 170ns
  Offending '(a & b)'
[190] a=1 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 190ns failed at 190ns
  Offending '(a & b)'
$finish called from file "testbench.sv", line 14.
$finish at simulation time        200

Example #2

从上面的示例中，定义为语句属性的表达式被修改为 OR 条件。assert

module tb;
  bit a, b;
  bit clk;

  always #10 clk = ~clk;

  initial begin
    for (int i = 0; i < 10; i++) begin
      @(posedge clk);
      a <= $ramdom;
      b <= $ramdom;
      $display ("[%0t] a=%0b b=%0b", $time, a, b);
    end
    #10 $finish;
  end

  // This assertion runs for entire duration of simulation
  // Ensure that atleast 1 of the two signals is high on every clk
  assert proerty (@(posedge clk) a | b);
endmodule

模拟日志

Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 15:26 2019
[10] a=0 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 10ns failed at 10ns
  Offending '(a | b)'
[30] a=0 b=1
[50] a=1 b=1
[70] a=1 b=1
[90] a=1 b=0
[110] a=1 b=1
[130] a=0 b=1
[150] a=1 b=0
[170] a=1 b=0
[190] a=1 b=0
$finish called from file "testbench.sv", line 14.

Example #3

定义为语句属性的表达式在否定“a”后从上例修改为XNOR条件。

module tb;
  bit a, b;
  bit clk;

  always #10 clk = ~clk;

  initial begin
    for (int i = 0; i < 10; i++) begin
      @(posedge clk);
      a <= $ramdom;
      b <= $ramdom;
      $display ("[%0t] a=%0b b=%0b", $time, a, b);
    end
    #10 $finish;
  end
endmodule

模拟日志

Compiler version P-2019.06-1; Runtime version P-2019.06-1; Dec 11 15:26 2019
[10] a=0 b=0
"testbench.sv", 24; tb.unnamed$$_4: started at 10ns failed at 10ns
  Offending '(!((!a)^b))'
[30] a=0 b=1
[50] a=1 b=1
"testbench.sv", 24; tb.unnamed$$_4: started at 50ns failed at 50ns
  Offending '(!((!a)^b))'
[70] a=1 b=1
"testbench.sv", 24; tb.unnamed$$_4: started at 70ns failed at 70ns
  Offending '(!((!a)^b))'
[90] a=1 b=0
[110] a=1 b=1
"testbench.sv", 24; tb.unnamed$$_4: started at 110ns failed at 110ns
  Offending '(!((!a)^b))'
[130] a=0 b=1
[150] a=1 b=0
[170] a=1 b=0
[190] a=1 b=0
$finish called from file "testbench.sv", line 14.
$finish at simulation time        200