I am taking a course going over SVA (specifically the followed by operator) and came across an example I couldn’t quite make sense of. So the example was how to use the followed by operator in conjunction with the followed by operator to create liveness covers. The example was as follows:
cover property (a #-# always 1);
It was said that in formal this would prove you can have a occurring, and from a occurring have an infinite length trace. This waveform was an example from the formal tool cover property:
So the thing that I am struggling to understand is what example the “always 1” is doing in the example. In trying to understand the example I references the LRM section 16.12.9 on the followed-by operator. After looking at what the LRM said I was only more confused. It said that
sequence_expr #-# property_expr
is equivalent to
not (sequence_expr |-> not property_expr)
So, for the example, it should be equivalent to:
not (a |-> not always 1)
So “always 1” should be true at all points; and since it is being negated with “not”, wouldn’t that mean that the consequent always evaluates to false?
And since the whole thing is negated with a not doesn’t that mean the expression only passes when a is true?
To give a more basic example to demonstrate what I am thinking.
say you have the following:
property exp;
@(posedge clk) (A |-> B);
endproperty
It should lead to the following truth table:
| A | B | exp | not(exp) |
|---|---|---|---|
| 0 | 0 | Pass | Fail |
| 0 | 1 | Pass | Fail |
| 1 | 0 | Fail | Pass |
| 1 | 1 | Pass | Fail |
The only condition property not(exp) passes is when A is 1 and B is 0. So if we made B = 0, then this property would always fail except when A = 1, correct?
So the only condition where not (a |-> not always 1) (and (a #-# always 1) since they should be equivalent) is one where a is always true? Which is why I don’t understand the formal cover example, where the cover is proven by an example where A goes high then low for infinity.