Hardware Reference
In-Depth Information
property
p_check_data_xfer(
1
local input
dataType l_dataModel [MAX_BEATS]
2
);
3
int unsigned
j=0;
4
(
5
(!retry && !(dataValid && complete))
6
throughout
dataValid[->1],
7
j++
8
)[
*
]
9
##1 (!retry && !dataValid)[
*
]
10
##1 (dataValid, j++)
11
|->
12
(
13
j <= MAX_BEATS
14
and
data == l_dataModel[j-1]
15
and if
(!retry && complete)
16
nexttime
!dataValid
17
);
18
endproperty
19
property
p_check_retried_data_xfer(
20
local input
dataType l_dataModel [MAX_BEATS]
21
);
22
(
23
( !(dataValid && complete)
throughout
retry[->1] )
24
or
25
(
26
(!retry && !(dataValid && complete))[
*
]
27
##1 dataValid && complete
28
##0
first_match
(##[0:1] retry)
29
)
30
)[+]
31
|=> p_check_data_xfer(l_dataModel);
32
endproperty
33
property
p_retry_check_non_rec;
34
dataType l_dataModel [MAX_BEATS];
35
(start, l_dataModel = dataModel)
36
|=>
37
sync_reject_on
(start)
38
(
39
p_check_data_xfer(l_dataModel)
40
and
41
p_check_retried_data_xfer(l_dataModel)
42
);
43
endproperty
44
a_retry_check_non_rec:
assert property
(p_retry_check_non_rec);
45
Fig. 17.15
Nonrecursive encoding of retry protocol checks
The remainder of this section provides an alternative, nonrecursive encoding of
the retry protocol checks. The encoding is shown in Fig.
17.15
. The main property,
p_retry_check_non_rec
, is similar to
p_retry_check
. It captures the data model
Search WWH ::
Custom Search