What happen if the antecedent occurs or it is true, but the consequent will never occur?

SystemVerilog
1

I have the following assertion:

assert property (@(psedge clk) req |-> ##[0:$] grnt);

I have doubts about the following two scenarios.

  1. In [0:$] how $ is decided by the tool? When will the $ actually occur for the tool?
  2. If the req will occur and grnt will never occur till the $. What will happen?
  3. If the req will never occur?
  4. So basically, how can we generalize the situation that (a) the antecedent will be true, but the consequent will never occur & (b) the antecedent will never be true?
2

  1. 0:$ indicates that grnt can occur at any clock once req is true ( incl. same clk due to |-> ). Tool will essentially check for ‘grnt’ to occur till end of simulation

  2. It’s an incomplete attempt with a non-vacuous pass ( as ‘req’ occurred )

  3. It’s an incomplete attempt with a vacuous pass ( as ‘req’ never occurred )

  4. (a) same as 2)

  5. (b) same as 3)

3

For the case 2 why not it will fail because the Manager sent the ‘req’ and the subordinate is not able to fulfill the ‘ack’ till the end of simulation.
You want to say that incomplete attempt with a non-vacuous pass = Fail.

4

No, there is no failure if ‘grnt’ was never found asserted

It won’t fail as it’s actively looking for ‘grnt’ to be true.

If your expect ‘grnt’ to occur in 100 clocks then you should write consequent as ##[0:100] grnt

Now the assertion would fail ( at 100th clock ) if ‘grnt’ isn’t asserted in 100 clocks

Ideally there would be max expected time for assertion of ‘grnt’

5

What you seem to be asking about is referred to as a liveness property: a scenario that is bound to eventually happen.

SystemVerilog has two types of assertions/properties/sequences: weak and strong. weak is considered a vacuous pass if there’s no match; it becomes true only after a match is found. On the other hand, a strong property fails if there’s no match, as it remains false even in the absence of a match.

The assertion you wrote is weak. If req never occurs or grnt never occurs, there is no failure; there is a vacuous pass. For a formal tool, [0:$] is unbounded; it searches indefinitely, limited only by the CPU resources you give it. But for dynamic simulation, [0:$] means until the end of the simulation.

If your requirement is: for each request, there must be a grant, you could write

assert property (@(psedge clk) $rose(req) |-> strong(##[0:$] grnt) );

or more descriptively

assert property (@(psedge clk) $rose(req) |->   s_eventually( grnt) );

Note that if you never receive a request, that shouldn’t be considered a failure. Not every test might trigger a request. When you compile and merge all your coverage data, you’ll find that this assertion never passed if there was never a request.

6

Hello Sir,

Would incomplete be a correct word to describe 2 and 3 ?

In coverage report I believe both of these scenarios would be uncovered, however does a tool / LRM further differentiate between these two ?

7

The LRM never formally defines an assertion as being complete or incomplete. Generally, an assertion is thought of as having an attempt, failure, vacuousness success, or non-vacuous success. A weak property that has been attempted but resulted in neither success nor failure may be considered incomplete. Strong properties, on the other hand, must either fail or pass, and there is no such thing as an incomplete strong property.

The LRM never mentions the fact that coverage is collected on the assert directive the same as a cover directive. Tools are required to record and report the number of attempts, vacuous, successes, and non-vacuous successes.