Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 114

a1: assert property (@( posedge clk) rdy |-> !rst);

Discussion: When both antecedent and consequent are Boolean, the suffix implica-
tion is equivalent to the logical implication:
a2: assert property (@( posedge clk) rdy -> !rst);
Of course, it is illegal to use a suffix implication in a Boolean expression.
Logical implications may be used in all kinds of assertions: immediate, deferred,
and concurrent, while suffix implications are allowed in concurrent assertions only.
t

Example 6.18. done must be asserted in the next clock tick after sent has been
asserted.

Solution: This assertion means that if in some clock tick sent has been asserted
then at the next clock tick done should be asserted. There are several possibilities
to divide this property into an antecedent and a consequent. We can say that the
antecedent is sent , and the consequent is done starting from the next clock tick.
The resulting assertion will be:

a1: assert property (@( posedge clk) sent |-> nexttime done);
The same intent may be expressed using sequential property in the consequent:
a2: assert property (@( posedge clk) sent |-> ##1 done);
We can move the delay into the antecedent to get the same effect:

a3: assert property (@( posedge clk) sent ##1 1 |-> done);
Note that assertion

a4_illegal: assert property (
@( posedge clk) sent nexttime 1 |-> done);
is illegal since the antecedent of a suffix implication is a sequence, not a property,
and using property operator nexttime is forbidden in sequences.
Of course, the best way to implement the same assertion is using non-overlapping
implication as shown below.

a5: assert property (@( posedge clk) sent |=> done);
Assertion a5 is equivalent to assertion a3 by the definition of the nonoverlapping
implication.

t

Example 6.19. In Example 6.18 we showed that it is possible to move a unit
delay from antecedent to consequent and vice versa when the first operand in the
consequent (or the last one in the antecedent) is 1. However, in the case of an
arbitrary operand this is wrong. For example, property write ##1 done |=> read
means that if done follows write then read must be asserted in the next clock
tick after done .Ifthereisno done after write the property passes. Property
write |=> done ##1 read means a different thing: each write must be followed
byaseriesof done and read .Ifthereisno done after write the property fails. t