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

sequence s_and_ambiguous;

1

bit l_v;

2

(

3

(a[->1], l_v = e)

4

and

5

(b[->1], l_v = f)

6

) // SF5: l_v does not flow out, becomes unassigned

7

##1 c == l_v; // illegal

8

reference to l_v endsequence

9

Fig. 16.12 Local variable becomes unassigned due to ambiguity of value after and

sequence s_and_unambiguous;

1

bit l_va, l_vb;

2

(

3

(a[->1], l_va = e)

4

and

5

(b[->1], l_vb = f)

6

)

7

##1 c == l_va || c == l_vb;

8

endsequence

9

Fig. 16.13 Assigning to distinct local variables in the operands of and

sequence s_or_ambiguous;

1

bit l_v;

2

( // DF: l_v does not flow in

3

(a[->1], l_v = e)

4

or

5

b[->1] // SF1: l_v does not flow out

6

) // SF4: l_v does not flow out, becomes unassigned

7

##1 c == l_v; // illegal reference to l_v

8

endsequence

9

Fig. 16.14 Local variable becomes unassigned due to ambiguity of value after or

value upon match of the and . According to Rule IF7 , l_v does not flow out of the
and subsequence, and as a result l_v becomes unassigned in Line 7 . The reference
to l_v in Line 8 is therefore illegal.
SF5 applies similarly to sequence operators intersect and within . Therefore,
when coding local variable assignments in operands of sequence and , intersect ,
or within , do not make assignments to a single local variable in more than
one operand. The ambiguous example from Fig. 16.12 can be recoded using
two local variables as shown in Fig. 16.13 . Note, in particular, that the compa-
rison to c in Line 8 has been disambiguated in Fig. 16.13 as the disjunction
c == l_va || c == l_vb .
Figure 16.14 shows a different problem occurring with assignments in operands
of a sequence or . In this example, l_v is not assigned before the or , and it is
assigned in only one operand of the or (Line 4 ). The semantics of sequence or
specifies that if either operand subsequence matches, then there is a match of the