Mechanics of Local Variables - SVA: The Power of Assertions in SystemVerilog - page 361

property p_data_and_parity;

1

dataType l_data;

2

parityType l_parity;

3

start ##1

4

(

5

(dataValid, l_data = data, l_parity = parity)

6

within complete[->1]

7

)

8

|-> parityOK(l_data, l_parity);

9

endproperty

10

Fig. 16.4 Data and parity check

of dataValid and hold them for comparison with the corresponding values at the
second occurrence of dataValid . If the corresponding values are equal, then the
overall sequence matches.
In general, the evaluation of the right-hand side of a local variable assignment
follows the rules for evaluation of expressions within a concurrent assertion. After
resolving the terms of the expression through elaboration (including argument
passing, module instantiation, bind instantiation, etc.), sampled values are used for
those terms that are not local variables, while current values are used for terms
that are local variables. These rules apply to declaration assignments for body local
variables and initialization assignments for argument local variables.
Each evaluation attempt of a named sequence or property gets its own, private
copy of all the declared local variables for use within that evaluation. Local variables
are thus “local” to an individual thread of evaluation, and variables for one thread
of evaluation cannot be referenced in another thread of evaluation. The examples
presented so far in this chapter have required only one copy of each local variable
per evaluation attempt. In general, evaluation of a sequence or property may involve
branching into subevaluations. Part of the power of local variables is that their
semantics includes automatic allocation of additional copies when needed to store
multiple values arising from such subevaluations. Consider the example in Fig. 16.4 .
This property checks that for every occurrence of dataValid that happens after
start and not later than complete , the values of data and parity that are present
with dataValid satisfy the condition encoded in the function parityOK . The local
variable assignments are attached to the Boolean subsequence dataValid , and the
resulting sequence is the first operand of the within operator. The within sequence
is itself part of the antecedent of |-> . The semantics of |-> requires that every match
of its antecedent result in a check of its consequent. Because dataValid may occur
at multiple points within the interval of matching of complete[->1] , there may be
multiple matches of the antecedent, and each such match will have its own copy of
the local variables to store the values of data and parity from the particular point
that dataValid occurred for that match.
Figure 16.5 shows a possible waveform for this property. Only the values of data
and l_data are shown, since the timing of the local variable capture for l_parity
is the same. start occurs at time 20 and complete occurs at time 90. Between
them there are three occurrences of dataValid , at times 30, 50, and 70. Therefore,