012 断言（Assertions）

Posted 2022-12-14 SilentLittleCat

• Immediate Assertions：立即断言
• Concurrent Assertions：并行断言

Immediate Assertions

//+++++++++++++++++++++++++++++++++++++++++++++++++
// DUT With Immediate assertions
//+++++++++++++++++++++++++++++++++++++++++++++++++
module assert_immediate();

reg  clk, grant, request;
time current_time;

initial begin
  clk = 0;
  grant   = 0;
  request = 0;
  #4 request = 1;
  #4 grant = 1;
  #4 request = 0;
  #4 $finish;
end

always #1 clk = ~clk;
//=================================================
// Assertion used in always block
//=================================================
always @ (posedge clk)
begin
  if (grant == 1) begin
     CHECK_REQ_WHEN_GNT : assert (grant && request) begin
        $display ("Seems to be working as expected");
     end else begin
        current_time = $time;
        #1 $error("assert failed at time %0t", current_time);
     end
  end
end

endmodule

	
 Info: "assert_immediate.sv", 21: 
  assert_immediate.CHECK_REQ_WHEN_GNT: at time 9
 Seems to be working as expected
 Info: "assert_immediate.sv", 21:
  assert_immediate.CHECK_REQ_WHEN_GNT: at time 11
 Seems to be working as expected
 "assert_immediate.sv", 21: 
      assert_immediate.CHECK_REQ_WHEN_GNT: 
 started at 13s failed at 13s
         Offending '(grant && request)'
 Error: "assert_immediate.sv", 21: 
 assert_immediate.CHECK_REQ_WHEN_GNT: at time 14
 assert failed at time 13
 "assert_immediate.sv", 21:
       assert_immediate.CHECK_REQ_WHEN_GNT: 
 started at 15s failed at 15s
         Offending '(grant && request)'

Concurrent assertions

并行断言描述跨时间的信号特征，它在时钟刻度（Clock tick）处对信号进行采样，判断断言是否成立

//+++++++++++++++++++++++++++++++++++++++++++++++++
//   DUT With assertions
//+++++++++++++++++++++++++++++++++++++++++++++++++
module concurrent_assertion(
  input wire clk,req,reset, 
  output reg gnt);
//=================================================
// Sequence Layer
//=================================================
sequence req_gnt_seq;
  // (~req & gnt) and (~req & ~gnt) is Boolean Layer
  (~req & gnt) ##1 (~req & ~gnt);
endsequence
//=================================================
// Property Specification Layer
//=================================================
property req_gnt_prop;
  @ (posedge clk) 
    disable iff (reset)
      req |-> req_gnt_seq;
endproperty
//=================================================
// Assertion Directive Layer
//=================================================
req_gnt_assert : assert property (req_gnt_prop)
                 else
                 $display("@%0dns Assertion Failed", $time);
//=================================================
// Actual DUT RTL
//=================================================
always @ (posedge clk)
  gnt <= req;

endmodule

//+++++++++++++++++++++++++++++++++++++++++++++++
//   Testbench Code
//+++++++++++++++++++++++++++++++++++++++++++++++
module concurrent_assertion_tb();

reg clk = 0;
reg reset, req = 0;
wire gnt;

always #3 clk ++;

initial begin
  reset <= 1;
  #20 reset <= 0;
  // Make the assertion pass
  #100 @ (posedge clk) req  <= 1;
  @ (posedge clk) req <= 0;
  // Make the assertion fail
  #100 @ (posedge clk) req  <= 1;
  repeat (5) @ (posedge clk);
  req <= 0;
  #10 $finish;
end

concurrent_assertion dut (clk,req,reset,gnt);

endmodule

##、$

// a为1后，下个触发沿b为1
a ##1 b

这种也可以

// a为1后，2-5个触发沿后b为1
a ##[2:5] b

// $表示仿真结束
// a为1后，0-无穷个触发沿后b为1
a ##[0:$] b

Repetition Operators

Consecutive repetition ( [* )

// a为1后，1个触发沿后，有1-2个连续的1
a ##1 b[*1:2]

Goto repetition ( [-> )

// a为1后，1个触发沿后，有2个可以不连续的1
a ##1 (b[->2]) ##1 c
a ## 1 ((!b[*0:$]  ##1  b) [*2])  ##1 c

Nonconsecutive repetition ( [= )

// a为1后，1个触发沿后，有2个可以不连续的1，后面可以跟0，再续1
a ##1 (b[=2]) ##1 c
a ## 1 ((!b[*0:$]  ##1  b) [*2])  !busy[*0:$]  ##1 c

$sampled、$rose、$fell、$stable、$past

• $sampled：对当前值采样，多余
• $rose：信号最低位变为1
• $fell：信号最高位变为0
• $stable：信号与上个时钟时间相同
• $past：返回n个时钟前的值

// a变为1，且a的上一个状态是0（a：0 -> 1），下一个时钟沿b做同样的变化
property system_prop;
  @ (posedge clk) 
      ($rose(a) && $past(!a,1)) |=> 
         ($rose(b) && $past(!b,1));
endproperty

Binary Operators：and、intersect 、or

• and：两个事件都匹配，且同时开始
• intersect：两个事件都匹配，且同时开始，同时结束
• or：任意一个事件匹配

property prop;
  @ (posedge clk) 
    req |-> a and b;
    // req |-> a intersect b;
    // req |-> a or b;
endproper

Match Operators：throughout、within

property prop;
  @ (posedge clk) 
    // b之内a都有效（可能理解有错，待测试）
    req |-> a throughout b;
    // a的有效在b的有效之内
    // req |-> a within b;
endproper

disable iff

如果断言成立，disable一些属性，常用于复位

property req_gnt_prop;
  @ (posedge clk) // At every posedge clk
    disable iff (reset) // disable if reset is asserted
      req |=> req_gnt_seq;
endproperty

assert、assume、cover

• assert：断言
• assume：该语句将属性指定为验证环境的假设。 这对于正式的验证工具更有用
• cover：该语句为了覆盖而监视属性。 覆盖可以在模拟结束时报告

bind

将测试与RTL设计绑定，使RTL和测试可以分开

expect

expect与语法中的assert相同，但是expect在过程块中使用，并且等待属性评估为true或false

|->、|=>

// a、b同时为1
property req_gnt_prop;
  @ (posedge clk) 
    a |-> b;
endproperty

// a为1，b下个时钟为1
property req_gnt_prop;
  @ (posedge clk) 
    a |=> b;
endproperty