Hardware Reference
In-Depth Information
16.3
Assigning to Local Variables
The fundamental capability provided by local variables is to enable an assertion
to capture the value of an expression at a specified point in its evaluation and
store that value for later reference, perhaps after further modification. This section
discusses rules for assigning to local variables. The declaration and initialization
assignments introduced in Sects.
16.1
and
16.2
are particular cases of assignments
to local variables. They must follow the rules presented here.
A local variable assignment may be attached to a subsequence of a named
sequence or property. The local variable assignment is written after the subsequence,
separated by a comma, and the pair is enclosed in parentheses. The subsequence
must not admit an empty match. Whenever the subsequence matches in the course
of evaluation of the named sequence or property, the local variable assignment is
performed. The result of attaching a local variable assignment to a subsequence is
always a sequence, even if the subsequence were itself a Boolean. Here is a simple
example:
property
p_ttype_vs_data;
transType l_ttype;
(start, l_ttype = ttype)
##1 (dataValid
within
complete[->1])
|-> ttypeAllowsData(l_ttype);
endproperty
The local variable assignment
l_ttype = ttype
has been attached to the Boolean
subsequence
start
. Whenever
start
is tested and evaluates to true, the Boolean
subsequence matches and the local variable assignment is performed, capturing the
value of
ttype
for later reference in the call to the function
ttypeAllowsData
.This
property checks that if
dataValid
occurs after
start
and not later than
complete
,
then the transaction type specified in
ttype
at the time of
start
is one that allows
data as encoded in
ttypeAllowsData
.
Multiple local variable assignments may be attached to a single subsequence.
The local variable assignments are performed in order whenever the subsequence
matches.
sequence
s_compare_two_data_and_parity;
dataType l_data;
parityType l_parity;
start
##1 (dataValid[->1], l_data = data, l_parity = parity)
##1 dataValid[->1]
##0 data == l_data && parity == l_parity;
endsequence
This sequence compares the values of
data
and
parity
from the first two occur-
rences of
dataValid
after
start
. Two assignments have been attached to the first
goto subsequence
dataValid[->1]
:
l_data = data
and
l_parity = parity
.
The local variables capture the values of
data
and
parity
from the first occurrence
Search WWH ::
Custom Search