Recursive Properties - SVA: The Power of Assertions in SystemVerilog - page 391

10 20 30 40 50 60 70 80 90 100

clk

start

dataValid

complete

retry

Fig. 17.12 Waveform for retry protocol

7. At any time subsequent to start and no later than the cycle after the last
data beat, an occurrence of retry signals that the data transfer is forced to
retry. This means that no further data beats in the current sequence may be
transferred, and the data transfer must begin the sequence again, starting with
dataModel[0] . The transaction itself does not restart after retry, only the data
transfer. Specifically, the transaction does not reassert start and dataModel is
not observable after retry . There is no limit to the number of times the data
transfer may be forced to retry.
8. The overall write transaction completes in the cycle after the last data beat
provided retry does not occur in that cycle. A write transaction is said to be in
flight beginning in the cycle after start and continuing up to and including the
cycle that the transaction completes.
9. Write transactions must be sequential. More precisely, start must not occur
while a write transaction is in flight.
10. If dataValid , complete ,or retry occurs while no write transaction is in flight,
then it is ignored.

Figure 17.12 shows a waveform for the control signals of the retry protocol.
A transaction starts at time 20. Two data beats occur at times 30 and 40, and
complete is signaled at time 40. At time 50, retry occurs, so the data transfer
must start again. Two data beats are repeated at times 70 and 90, and complete is
signaled at time 90. Since retry does not occur again, the transaction completes at
time 100.
Note that the protocol makes no requirement on the number of data beats in a
retried data transfer. A retried data transfer might have fewer or more data beats
than a previous data transfer, even if the previous data transfer signaled complete .
However, for each beat that occurs in a retried data transfer, the data must match the
value predicted by dataModel .
Figure 17.13 shows a flow diagram to check the retry protocol. The flow begins
with start . In the cycle of start , dataModel is captured. The flow then advances
to the next cycle and invokes synchronous reject on start .If start occurs while
the check is ongoing, then the check fails (rule 9 ). The counter i is then initialized