Search code examples
system-verilogassertionsystem-verilog-assertions

Meaning of |-> 1[0:$] in assertions

Usage example:

state==ACTIVE1 |-> 1[0:$] ##1 state==ACTIVE2

The problem the assertion is trying to solve is: if the state machine reaches state=ACTIVE1, it will eventually reach state=ACTIVE2.

Any idea what |-> 1[0:$] actually means?

Also, is there a better way to do the same?

Solution

  • In SVA 1 is effectively a wildcard, because it is, by definition, true. So it matches anything.

    <expression>[<number or range>] is the SVA repetition operator.

    $ means "infinity".

    So, 1[0:$] means "anything zero or more times".

    Is there a better way to do it? Yes. Here are some other ways to do it that suffer all suffer from the same problems that your example does:

    state==ACTIVE1 |-> ##[0:$] state==ACTIVE2
state==ACTIVE1 |-> eventually state==ACTIVE2

    What are these problems?

    (i) If there are lots of ACTIVE1s and no ACTIVE2s then more and more checks will be started (ie threads spawned), which slows down your simulation. This is a problem with the use of $ or eventually on the right hand side (the consequent or condition).

    (ii) Your assertion can never fail: it doesn't matter whether there has been no ACTIVE2 by the heat death of the universe, your assertion will not fail. Here is a compromise assertion, a so-called strong property:

    state==ACTIVE1 |-> s_eventually state==ACTIVE2

    The s_ stands for "strong". Now, if your assertion has not passed by the end of the simulation, that is considered a fail.