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

Solution: This assertion means that if start is asserted and if two clock ticks later
send is asserted, then in three clock ticks after send was asserted, ack must be
asserted. This can be directly mapped into nested implications:

a1: assert property (@( posedge clk)
start |-> ##2 send |-> ##3 ack);

Discussion: Nested suffix implication is unambiguous: the antecedent of the
outermost implication is start , and not start |-> ##2 send because the latter
expression is a property, and not a sequence, whereas the antecedent must be a
sequence.
The same assertion may be reformulated in the following way: each time send
is issued two cycles after start , ack should arrive three cycles after send , and the
assertion can be rewritten as

a2: assert property (@( posedge clk) start ##2 send |-> ##3 ack);
Both forms are equivalent. Usually the form with a single implication is more
intuitive than the one with nested implications, and it is easier to debug.
The rule of transforming nested implications works with appropriate modifi-
cations for any initial delays in the consequent. For example, r |=> s |=> p is
equivalent to r ##1 s |=> p , and r|->s|->p is equivalent to r ##0 s |-> p .

t

6.4.2 Examples

In this section, we provide several important examples illustrating use of various
sequence and property operators combined with suffix implication.

Example 6.22. Request req should be active until grant is asserted.
Solution: This assertion may be formulated as “Whenever the request is high, it
should remain high until (not including) grant is asserted”:
a1: assert property (@( posedge clk) req |-> req until grant);

Discussion: If the request should remain asserted also in the first clock tick when
the grant is asserted the assertion should be modified as:

a2: assert property (@( posedge clk)
req |-> req until_with grant);

t

Efficiency Tip. Boolean antecedents in suffix implication are efficient in FV, but
they may be not very efficient in simulation when the consequent requires a long
time for its completion. See Chap. 7 and Sect. 19.3 for a detailed discussion.

Example 6.23. Request req must be granted. This assertion means that each time
request req is high, grant gnt should be high in some clock tick in the future.