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

start

capture
dataModel

goto next cycle

synchronous
reject on start

i=0

goto
dataValid or
retry

dataValid

yes

check data
==
dataModel[i]

goto next cycle

check i<
MAX - BEATS-1 ;
i = i+1

yes

retry goto next cycle

no

no

complete yes

yes

goto next cycle;
check
!dataValid

retry

no

done

Fig. 17.13 Flow diagram for retry protocol checks

to zero, indicating that the check expects the first data beat. The flow then advances
to the nearest occurrence of dataValid or retry .If dataValid occurs, the flow
checks that data equals dataModel[i] .If retry occurs, the flow advances to
the next cycle and resets i to zero to begin the data transfer again. If complete
has not also occurred, then the flow increments i , checks that the result is not too
big in comparison with MAX_BEATS , advances a cycle, and returns to look for the
next dataValid or retry .If complete has also occurred, then the data transfer
is complete and the flow advances one more cycle, where it checks that dataValid
does not occur and checks for retry at the last opportunity. If retry does not occur,