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

sequence s_or_unambiguous;

1

bit l_v = 1'b0;

2

(

3

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

4

or

5

b[->1]

6

)

7

##1 c == l_v;

8

endsequence

9

Fig. 16.15 Local variable assigned before or

sequence s_nested_ambiguity;

1

bit l_v = 1'b0;

2

(

3

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

4

or

5

(

6

(b1[->1], l_v = f1)

7

and

8

(b2[->1], l_v = f2)

9

) // SF5: l_v does not flow out

10

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

11

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

12

endsequence

13

Fig. 16.16 Nested structure results in local variable becoming unassigned

or , and evaluation continues for each such match. After Line 7 , it is not known
which operand of the or matched, and so it is not known whether l_v has been
assigned. According to Rule IF6 , l_v does not flow out of the or , and l_v becomes
unassigned in Line 7 . The reference to l_v in Line 8 is therefore illegal.
The situation in Fig. 16.14 can be remedied by ensuring that l_v will be assigned
a value no matter which operand of the or matches. This can be done by assigning
a value to l_v prior to the or or by assigning a value to l_v in the second operand
(Line 6 ). Figure 16.15 uses a declaration assignment to provide a value to l_v prior
to the or .
The flow rules must be applied recursively to sequences and properties with
nested structure. Figure 16.16 shows an example in which the second operand of
an or subsequence is itself an and subsequence. According to IF7 , l_v does not
flow out of the and (Line 10 ). Even though l_v is assigned before the or (Line 2 )
and is assigned within each operand of the or , IF6 then implies l_v does not flow
out of the or and becomes unassigned in Line 11 . The reference to l_v on Line 12
is therefore illegal.