Hardware Reference
In-Depth Information
property
p_ttype_vs_beats;
1
transType l_ttype;
2
int
numBeats = 0;
3
(start, l_ttype = ttype) ##1
4
(
5
(dataValid[->1], numBeats++)[
*
]
6
##1 !dataValid[
*
]
7
intersect
8
complete[->1]
9
)
10
|-> numBeatsOK(l_ttype, numBeats);
11
endproperty
12
Fig. 16.10
Illustrating local variable flow, reference, and reassignment
ttype != l_ttype
in Line
5
compares
PRG != INV
and succeeds. At time 80,
though, this thread fails since Line
5
compares
INV != INV
, and so the overall
evaluation beginning at time 20 fails. The evaluation that begins at time 40 succeeds
since its two checks of Line
5
compare
INV != PRG
at time 80 and
READ != PRG
at time 90.
16.4.1
Local Variable Flow
To understand more thoroughly where a local variable may be referenced and what
value will be yielded, we need to explore in more detail how the scope of the
local variable extends into various subsequences and subproperties and how the
value stored in the local variable is carried along and changed in the corresponding
subevaluations. A local variable is said to
flow into
a subsequence or subproperty if
it is assigned (i.e., has a value) when evaluation of the subsequence or subproperty
begins. A local variable is said to
flow out of
a subsequence if it is guaranteed to be
assigned (i.e., to have a value) upon reaching the end of a match of the subsequence.
In general, if a local variable flows into a subsequence or subproperty, then the
local variable may be referenced within that subsequence or subproperty provided
the local variable remains assigned at the point of reference. (See Sect.
16.4.2
for a
discussion of how a local variable may become unassigned.) A reference to a local
variable yields the latest value assigned to it in the evaluation or subevaluation that
reaches the point of the reference. The latest assignment may have occurred in the
current time step. A local variable reference is always to the current value stored in
the variable.
As an example of local variable flow, reference, and reassignment, let us revisit
the property
p_ttype_vs_beats
, which is copied here in Fig.
16.10
. The property
has two local variables:
l_ttype
has no declaration assignment, while
numBeats
has a declaration assignment initializing its value to
0
. Therefore,
l_ttype
is
unassigned and does not flow into the body of the property in Line
4
, while
Search WWH ::
Custom Search