System verilog assertion to check that signal 'a' takes a value only when it has taken some other particular value before

SystemVerilog
,
10

In reply to alexandru_dinu:


module top;
  timeunit 1ns;  timeprecision 100ps;    
  `include "uvm_macros.svh"   import uvm_pkg::*;
  bit clk, c, d, reset_n=1'b1;
  int a, d2, d1; 
  // signal 'a' takes a value ''d2' only when it has already 
  // had the value ''d1' anytime before, during the simulation.
  // In other words, Once a new occurrence of a==d1 then sometime later 
  //  a==d2 with NO other a being equal to the stored value of d1. d1 is a one clock cycle duration.
  initial forever #10 clk = !clk;
  
  // @rose 0f a==d1, save d1. Starting from next cycle 'a' should not equal to that 
 // saved value until a==d2
  // Error flagged if a==stored value. 
  property p_a_is_d1_thend2; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($rose(a==d1), v=d1) |-> ##1  a!=v[*1:$] ##0 a==d2;  
  endproperty 
  ap_a_is_d1_thend2: assert property(p_a_is_d1_thend2);  

  // WITH ISSUES 
  // @rose 0f a==d1, save d1. Starting from next cycle 'a' should not equal to that 
 // saved value ANDed with a==d2
  // ISSUE: Error is NOT flagged if a==stored value before a==d2. 
  property p_HAS_ISSUES_a_is_d1_thend2; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($rose(a==d1), v=d1) |-> ##1  (a==d2 && a!=v)[->1]; 
  endproperty 
  ap_HAS_ISSUES_a_is_d1_thend2: assert property(p_HAS_ISSUES_a_is_d1_thend2);  

  /*  if c 1 bit signaled toggled (let's say from low to high, but the level reached by signal can be kept into a variable),
   and its high value is steady high for 8 clock cycles, it MUST be steady high another 90 clock cycles. */
   property p_c8_90; 
    bit[2:0] v; 
    @(posedge clk) disable iff(reset_n==0)  
      ($changed(c), v=c) ##1 c==v[*8] |->  ##1 c==v[*90];
  endproperty 
  ap_c8_90: assert property(p_c8_90);   
  

  initial begin
    repeat (200) begin
      @(posedge clk);
      if (!randomize(a, d1, d2, c) with {
        a  dist {1 := 1, 2 := 4, 3:= 4 };
        d1 dist {1 := 1, 2 := 2, 7:= 2 };
        d2 dist {5 := 1, 6 := 2, 7:= 2 };
        c  dist {1'b1 := 1, 1'b0 := 15 };
      })
        `uvm_error("MYERR", "This is a randomize error");
    end
    $finish;
  end
endmodule

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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: