User guide

23-19
SystemVerilog Assertion Constructs
a1: assert property (p3(sig3,sig4));
Here the property uses signals sig1 and sig2 in its sequential
expression, but signals sig3 and sig4 replace them in the assertion
declaration.
Implications
Property implications, contain a boolean or sequential expression,
called an antecedent, which must be true or match before VCS starts
to monitor the events in another sequence or sequential expression,
called the consequent, to see if that sequence matches.
There are two types of implications:
• Overlapping implications where the antecedent and the first event
in the declared sequence or sequential expression happen during
the same clock tick. For overlapping implications you enter the
|-> operator between the antecedent and the consequent.
• Non-overlapping implications where there is a clock tick delay
between the antecedent and the consequent. For
non-overlapping implications you enter the |=> operator between
the antecedent and the consequent.
The following are examples of the VCS implemented implication
constructs:
sequence s1;
sig1 ##1 sig2;
endsequence
property p1;
@(posedge clk) (sig3 || sig4) |-> s1;
endproperty