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