Systemverilog assertion a signal is true at least

Question

I met a problem when trying to write this assertion. I tried to assert the scenario that signal B must be true at least 1 occurrence after signal A is true.

The assertion I wrote is below:

example  : assert property(
       @(posedge clk) disable iff(reset)
       A |-> ##[0:$] B[->1]) else `uvm_error(....)

The problem is, if during the simulation signal B is never be true after A is true, the uvm_error is not executed. I expected it to be executed, and the simulation reports the message:

example: started at xxxxxxps not finished

It seems the assertion is not finished even the simulation reaches the end.

I looked up in google, there is a similar question: Assertion to check for the toggle (0->1) of a signal

I also tried use strong() operation, it did not help as well.

How to solve this problem?

Answer 1

Unfortunately, your solution depends on which simulator you are using. I tried four and got different behaviours on each.

I think your solution is this:

  example3  : assert property(
       @(posedge clk) disable iff(reset)
    A |-> s_eventually B)
    else 
      $error("%t - Assertion example3 failed", $time);

based on it working on two simulators and my understanding of SVA. On one simulator the $error statement in the action block actually gets executed and the message "Assertion example3 failed" is displayed; in another a generic error message is displayed.

The s_ stands for "strong". The assertion means that B must occur sometime before the end of the simulation.

Here is an MCVE. Your question would have been easier to answer had you included something like this.

module M;

  bit stop;  bit clk; initial while (!stop) #5 clk = ~clk;

  bit A, B;

  initial begin
    #20 A = 1;
    #10 A = 0;
    // #10 B = 1;
    #10 B = 0;
    #50 stop = 1;
  end

  example1  : assert property(
       @(posedge clk)
    A |-> B[->1]) 
    else 
      $error("%t - Assertion example1 failed", $time);

  example2  : assert property(
       @(posedge clk)
    A |-> eventually [0:7] B)
    else 
      $error("%t - Assertion example2 failed", $time);

  example3  : assert property(
       @(posedge clk)
    A |-> s_eventually B)
    else 
      $error("%t - Assertion example3 failed", $time);

   final
     $display("Finished!");

endmodule

https://www.edaplayground.com/x/2RtF