An Apology for Local Variables - SVA: The Power of Assertions in SystemVerilog - page 338

1 property p_fifo_data_check;
2 dataType data;
3 bit [0:$clog2(MAX_OUTSTANDING)] numAhead;
4 (start, data = dataIn, numAhead = outstanding)
5 ##1 (numAhead > 0 ##0 complete[->1], numAhead--)[ * ]
6 ##1 (numAhead == 0 ##0 complete[->1])
7 |->
8 dataOut == data;
9 endproperty
10 a_fifo_data_check: assert property (p_fifo_data_check);

Fig. 15.9 Encoding of FIFO protocol data check using local variables

at which the data check will be performed. Lines 5 and 6 cause the evaluation to
advance to the cycle of the data check and are discussed in detail below. Finally,
Line 8 performs the simple data comparison.
Line 5 does the job of advancing the evaluation through the occurrences of
complete that need to be skipped. This line deserves careful study. It begins with
##1 , which simply advances to the cycle after the occurrence of start . The rest of
the line is a repetition of zero or more occurrences of the sequence
(numAhead > 0 ##0 complete[->1], numAhead--)
Let us call this sequence the skipping sequence . The top-level structure of
the skipping sequence attaches the local variable assignment numAhead-- to the
subsequence
numAhead > 0 ##0 complete[->1]
In general, local variable assignments may be attached to any sequence that does
not admit an empty match. The assignment numAhead-- uses the decrement opera-
tor -- and behaves the same as numAhead = numAhead - 1 . The subsequence to
which it is attached begins with the Boolean condition numAhead > 0 , which is true
if and only if there remain occurrences of complete that need to be skipped. This
Boolean is fused via ##0 to the sequence complete[->1] , which advances to the
next occurrence of complete . Each match of the skipping sequence in the repetition
therefore behaves as follows:
￿ Confirm that numAhead > 0 , hence that there remains at least one occurrence of
complete that needs to be skipped.
￿ Advance to the next occurrence of complete by matching complete[->1] .
￿ Decrement numAhead .
Because numAhead is decremented for each match in the repetition, the skipping
sequence is matched at most a number of times equal to the value that was stored
in numAhead in Line 4 . In fact, as explained below, Line 6 forces the skipping
sequence to be matched exactly this number of times. It is possible that this number
is zero, meaning that no occurrences of complete need to be skipped. In this case,
no matches of the skipping sequence are possible, and the zero repetition case is
used to match Line 5 .