User guide

23-20
SystemVerilog Assertion Constructs
Property p1 contains an overlapping implication. It specifies checking
that
(sig3 && sig4) is true and if so, during the same clock tick,
checking to see if sig1 is true, and then, a clock tick later, checking
to see if sig2 is true.
property p2;
@(posedge clk) (sig1 ##1 sig2) |-> (sig3 ##1 sig4);
endproperty
Property p2 also contains an overlapping implication. In p2 the
antecedent is a sequential expression.
property p3;
@(posedge clk) (sig3 ##1 sig4) |=> ##1 (sig1 ##1 sig2);
endproperty
Property p3 contains a non-overlapping implication. The first event
is the sequential expression, sig1 being true, must happen one clock
tick after the antecedent expression is true.
Remember that a property is either true or false, so for a property to
be true, by default the antecedent must be true and the consequent
must succeed. If you include the keyword not between the
implication operator and the consequent, the property is true if the
consequent does not succeed, for example:
property p4;
@(posedge clk) (sig3 && sig4) |-> not (sig1 ##1 sig2);
endproperty
Property p4 is true if, when (sig3 && sig4) is true, sig1 is not true,
or if it is, one clock tick later, sig2 is not true.