Systemverilog assertion a signal is true at least 1 occurence during the simulation

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?

Your English says B needs to be true at least once after A is true, but your assertion is checking for A needing to be true at least once after B is true (ie the other way round). Which is correct? — Matthew Taylor
By the way: this A[->1] means the same as this ##[0:$] A[->1]. — Matthew Taylor
Sorry for the mistake, I have now corrected it. Thanks very much — Shuaiyu Jiang
Sorry: two more questions: what is happening? what do you want to happen? (I'm sorry - you speak very good English, but not quite good enough for me to be able to understand the answer to these two questions). — Matthew Taylor
It is my fault, I did not express my question clearly. The signal A and B I wrote was in a wrong order, my bad. — Shuaiyu Jiang

Matthew Taylor Matthew Taylor · Accepted Answer · 2018-05-31T08:39:55

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

Systemverilog assertion a signal is true at least 1 occurence during the simulation

1 Answers