SVA: throughout corner case | sig1 must be stable throughout sig2

SystemVerilog
, ,
6

In reply to Ankit Bhange:
Consider the following model where all 3 assertions are different. The annotated assertion thread viewer address cases that demonstrate why they are different. It is always preferable to test the assertions in a small model using constrained-random tests.


module top;
  timeunit 1ns;  timeprecision 100ps;    
  `include "uvm_macros.svh"
  import uvm_pkg::*;
  bit clk, sig1, sig2;
  
  initial forever #10 clk = !clk; 
  ap_sig1_stable_throughout_sig2 : assert property(@(posedge clk)  
     $rose(sig2) |=> ($stable(sig1)[*1:$] ##1 !sig2) intersect !sig2[->1]);    

 
  ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)       
     $rose(sig2) |=> $stable(sig1) until !sig2); // Need the |=> because the until is a property 

  ap_sig1_stable_throughout_sig2_B : assert property(@(posedge clk) 
    $rose(sig2) |=>  $stable(sig1) throughout (sig2[*1:$] ##1 $fell(sig2)) ); 

  initial begin
    repeat (200) begin
      @(posedge clk);
      if (!randomize(sig1, sig2) with {
        sig1 dist {1'b1 := 10, 1'b0 := 1};
        sig2 dist {1'b1 := 6,  1'b0 := 1};
      })
        `uvm_error("MYERR", "This is a randomize error");
    end
    $finish;
  end
endmodule

2148×900 156 KB

2148×900 156 KB

ap_sig1_stable_throughout_sig2 : assert property(@(posedge clk)
$rose(sig2) |=> (stable(sig1)[*1:] ##1 !sig2) intersect !sig2[->1]);

1638×903 136 KB

1638×903 136 KB

ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) until !sig2);

1920×1080 360 KB

1920×1080 360 KB

ap_sig1_stable_throughout_sig2_B : assert property(@(posedge clk)
$rose(sig2) |=> stable(sig1) throughout (sig2[*1:] ##1 $fell(sig2)) );

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: