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

10 20 30 40 50 60 70 80 90 100

clk

req

ack
err

Fig. 6.6 Overlapping implication

10 20 30 40 50 60 70 80 90 100

clk

req
ack
err

Fig. 6.7 Nonoverlapping implication

Example 6.20. If there is no acknowledgment ack within three clock ticks after
request req was issued, request req must be resent unless an error indicator err
is set.

Solution: From this formulation it is not clear when the request should be resent
exactly: in three or in four clock ticks? We will consider both cases (assertions a1
and a2 ) differing by the type of the implication:
a1: assert property (@( posedge clk)
req ##1 !ack[ * 3] |-> req || err);
a2: assert property (@( posedge clk)
req ##1 !ack[ * 3] |=> req || err);
The corresponding timing diagrams are shown in Figs. 6.6 and 6.7 .

t

6.4.1 Nested Implication

Suffix implications can be nested as illustrated in the following example.

Example 6.21. If start is asserted two clock ticks before send , then acknowledg-
ment ack should arrive in three clock ticks after send was asserted.