System verilog assertion on asynchronous signals

SystemVerilog
, ,
2

In reply to DChal:
You can use the following as a baseline. Note that as long as dat==ccheck, “a” must follow “b”.
See the notes on my assumptions.


module top;
    timeunit 1ns / 100ps;
    `include "uvm_macros.svh"
    import uvm_pkg::*;
    bit clk, a, b, dis;
    int dat, check;      
    initial forever #10 clk = !clk;
    
    // There is a need to define which time zone to reject.
    // For this model, I am assuming that the zone to rejet is 3ns 
    // after dat!check
    // During check, "b" must follow "a" within 2ns 
    // Am assuming that "a" occurs first ar at the same time as "b"  
    always begin
        @(dat != check)  begin 
            dis=1'b1; 
            #3; 
            dis=1'b0;
        end
    end
    property p_ab; 
        realtime t; 
        disable iff(dis) 
        @(a) (check==dat, t=$realtime) |-> @(b) $realtime-t <2ns &&  $realtime-t >=0;
    endproperty 
    ap_ab: assert property(p_ab);  

  
    initial begin
      repeat (200) begin
        @(posedge clk);
        if (!randomize(a, b, dat, check) with {
          a dist {1'b1 := 1, 1'b0 := 1};
          b dist {1'b1 := 1, 1'b0 := 2};
          dat dist {2 := 1, 3 := 2};
          check dist {2 := 1, 3:= 1};
        })
          `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) https://rb.gy/cwy7nb
  3. Papers: