Hardware Reference
In-Depth Information
typedef bit
[0:$clog2(MAX_OUTSTANDING)] counterType;
1
property
p_fifo_data_check_recur(
2
local input
dataType data,
3
local input
counterType numAhead
4
);
5
##1 complete[->1]
6
|->
7
if
(numAhead == 0)
8
dataOut == data;
9
else
10
p_fifo_data_check_recur(data, numAhead--);
11
endproperty
12
property
p_fifo_all_checks_recur(
13
local input
counterType outstanding
14
);
15
(start || complete)[->1]
16
|->
17
(
18
(1'b1, outstanding += start - complete)
19
|=> p_fifo_all_checks_recur(outstanding)
20
)
21
and
22
if
(start) (
23
(!complete && outstanding < MAX_OUTSTANDING)
24
and
p_fifo_data_check_recur(dataIn, outstanding)
25
)
else
( // complete
26
!start && outstanding > 0
27
);
28
endproperty
29
initial
30
a_fifo_all_checks:
assert property
(
31
p_fifo_all_checks_recur('0)
32
);
33
Fig. 17.11
Recursive encoding of all FIFO protocol checks using only local variables
4. At an occurrence of
start
, expected data for the associated write transaction
is available in the array
dataModel
.
dataModel
is an unpacked array of
MAX_BEATS
entries, each of type
dataType
. It is declared as
dataType dataModel [MAX_BEATS];
The
beats
of
the
transaction
must
transfer
the
data
in
the
sequence
dataModel[0]
,
dataModel[1]
, :::.
5. Subsequent to
start
, an occurrence of
dataValid
signals a data beat. Data
beats do not have to be consecutive. In a cycle in which
dataValid
occurs, the
data for the beat is carried on the signal
data
.
6. The last data beat for the data transfer is signaled by occurrence of
complete
together with
dataValid
.
complete
is meaningful only together with
dataValid
.If
complete
occurs without
dataValid
, then it is ignored.
dataValid
may not occur in the cycle after the last data beat.
Search WWH ::
Custom Search