Next Cycle Implication operator does not work

In reply to UVM_LOVE:
…"SVA testbench must be conducted on non-blocking domain. "
[Ben] Not quite. However, typically, signals are assigned nonblocking and occur in the NBA region. Doing a #10 a=1; with posedge(clk) changing at t is same time when “a” changes can be problematic. It is also not stylist, though it should work; this is because within a time step signals used in an assertin are sampled in the Preponed region with the value just before the time step. What would be better is to do something like
@(posedge clk) a=1; // or a <=1;
Assertion sample signals in the Preponed region
See my paper 3) Understanding Assertion Processing Within a Time Step (Horizons Feb 27, 2023 issue)

This paper goes into detail about how evaluation regions should be handled by a simulator as described in the SystemVerilog LRM; this should give you a better understanding of how assertions work.


// I do the following: 
initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    bit v_a, v_b, v_err;
    repeat (200) begin
      @(posedge clk);
      if (!randomize(v_a, v_b, v_err) with {
        a  dist {1'b1 := 1, 1'b0 := 1}; // *****CAN USE signal a 
        // a changes in the Active region ************ OK 
        v_b   dist {1'b1 := 1, 1'b0 := 2};
        v_err dist {1'b1 := 1, 1'b0 := 15};
      }) `uvm_error("MYERR", "This is a randomize error");
      
      if(v_err==0) b<=v_b; else b<=!v_b; 
       // b changes in the NBA region  ****************
    end
    $finish;
  end