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 doubt in the following two scenarios.

  1. In [0:\\] how '’ is decided by the tool? When actually the $ will 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) antecedent will true, but consequent will never occur & (b) antecedent will never happen 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’