User guide

23-21
SystemVerilog Assertion Constructs
Inverting a Property
The keyword not can also be used before the declared sequence or
sequential expression, or if it contains an implication, before the
antecedent, to make the property true, if it otherwise would be false,
or make the property false if it otherwise would be true. For example:
sequence s1;
sig1 ##1 sig2;
endsequence
property p1;
@(posedge clk) not s1;
endproperty
Property p1 is true if sig1 is never true, or if it is, one clock tick later
sig2 is never true.
sequence s2;
@(posedge clk2) sig4 ##1 sig5;
endsequence
property p2;
not s2;
endproperty
Property p2 is true if sig4 is never true, or if it is, one clock tick later
sig5 is never true.
property p3;
@(posedge clk) not (sig3 && sig4) |-> not sig1 ##1 sig2;
endproperty
Property p3 is true if the implication antecedent is never true, or if it
is, the consequent sequential expression succeeds. Notice here that
the keyword not occurs twice in the property.