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

16.4.3 Multiplicity of Matching with Local Variables

Without local variables, multiple matches of a sequence over the same interval of
a trace can usually be treated as the same. 8

For example, consider the following

assertion:

a_mult_match: assert property (
(a[ * 1:2] or b[ * 1:2]) |-> c

);
For each evaluation attempt, the antecedent sequence can either not match or match
over one or two cycles. If a and b are not mutually exclusive, then each match could
be of multiplicity either one or two. Checking of the consequent is obligated for
each match of the antecedent, but the consequent evaluation is the same for multiple
matches over the same interval. Therefore, a tool can simply keep track of which
intervals are matched by the antecedent and not distinguish multiple matches over
the same interval.
With local variables, the values stored in them can differentiate matches over the
same interval of a trace. If there are subsequent references to the local variables,
then tools must keep track of the different values in the local variables for multiple
matches over the same interval. The following code illustrates this situation:

property p_mult_match_loc_var;
byte l_v;
((a[ * 1:2], l_v = e) or (b[ * 1:2], l_v = f)) |-> g != l_v;
endproperty
a_mult_match_loc_var: assert property (p_mult_match);
Property p_mult_match_loc_var has the same possibilities for matching of its
antecedent as assertion a_mult_match . However, because different expressions are
assigned to the local variable l_v in the two operands of or , this local variable
can distinguish multiple matches over the same interval. Since l_v is referenced
in the consequent, tools must keep track of all of the various multiple matches
of the antecedent and the associated values of l_v . The checking performed by
a_mult_match_loc_var is equivalent to the following assertion:
a_mult_match_2: assert property (
(a|->g!=e)
and (b|->g!=f)
and (a[ * 2] |-> g != $past(e))
and (b[ * 2] |-> g != $past(f))

);

8 When collecting coverage for a cover sequence assertion statement, all matches must be
counted with the appropriate multiplicities.