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