Hardware Reference
In-Depth Information
10
20
30
40
50
60
70
80
90
100
clk
start
complete
dataValid
4'ha
4'hb
4'hc
4'hd
data
undefined
undefined
4'ha
l -
data 30
undefined
undefined
4'hb
ldata 50
-
undefined
undefined
4'hc
ldata 70
-
Fig. 16.5
Waveform for data and parity check
the evaluation of p_data_and_parity that starts at time 20 will obtain three copies
of l_data , one for each of the three occurrences of dataValid . These copies are
shown as l_data 30 , l_data 50 , and l_data 70
in the waveform, along with the values
of data that they capture.
16.3.1
Assignment Within Repetition
If the operand of a sequence repetition is a subsequence with a local variable
assignment attached, then the local variable assignment executes on each iterative
match of the subsequence. Such assignments can be used to count the number of
iterations or to compute aggregate values based on increments that are observable at
the successive matches of the subsequence.
Figure 16.6 shows an example of counting the number of iterations. 6 When
start occurs, the property stores the transaction type in the local variable l_ttype
(Line 4 ). The property checks that the number of occurrences of dataValid that
happen after start and not later than complete is allowable for the transaction type
according to the function numBeatsOK . The number of occurrences of dataValid
is counted in the local variable numBeats . numBeats is initialized to zero in its dec-
laration on Line 3 . The various occurrences of dataValid are matched by the goto
dataValid[->1] within the repetition on Line 6 , and numBeats is incremented
6 For formal verification, the int type of numBeats should be replaced with the type of smallest
bitwidth needed for the counter.
Search WWH ::




Custom Search