Hardware Reference
In-Depth Information
into a local variable when
start
occurs. Evaluation of the consequent begins in
the next cycle, where
sync_reject_on
(start)
is invoked and two properties are
instantiated and conjoined.
The first property is
p_check_data_xfer
, which checks the current data transfer
up to its completion or to an occurrence of
retry
. The antecedent of
|->
in Lines
5
to
11
is crafted to match at each occurrence of
dataValid
in the current data
transfer that is not strictly subsequent to an occurrence of
retry
or an occurrence of
dataValid && retry
. Lines
5
-
9
match zero or more occurrences of
dataValid
,
none together with
complete
. Throughout match of these lines,
retry
must not
occur. Lines
10
and
11
match one more occurrence of
dataValid
. In these lines,
retry
must not occur strictly before
dataValid
. The consequent of
|->
checks that
the counter
j
has not grown too large and that
data
is correct. Also, it checks that
if
dataValid
and
complete
occur without
retry
, then
dataValid
does not occur
in the next cycle.
The second property is
p_check_retried_data_xfer
. This property is respon-
sible for restarting
p_check_data_xfer
each time a data transfer is forced to retry.
The overall antecedent of
|=>
is a repetition of one or more matches of the sequence
in Lines
24
to
30
. That sequence encodes the condition that a data transfer is forced
to retry. The occurrence of
retry
may be strictly before
dataValid && complete
,
which matches Line
24
. Or the occurrence of
retry
may be concurrent with or
in the cycle after
dataValid && complete
. These cases match Lines
27
to
29
.
The antecedent has been arranged to avoid multiple matches, which could result in
redundant checking of the consequent. The consequent of
|=>
simply instantiates
p_check_data_xfer
to begin checking the data transfer again.
It should be clear that the sequential conditions in the antecedents of these
two properties are complex and prone to error in comparison with the recursive
encoding.
17.3
Restrictions on Recursive Properties
The coding flexibility afforded by recursive properties is tempered by four
restrictions on their use. The restrictions are intended to avoid recursive declarations
and instances that are problematic or whose semantics involves subtleties that are
beyond the scope of the current semantic framework for recursion. This section
quotes the restrictions from the LRM and elaborates briefly on the rationale
for them.
Search WWH ::
Custom Search