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

property p_flow_analysis;

1

byte l_v;

2

(

3

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

4

within

5

b[->1]

6

)

7

#=#

8

(

9

(c == l_v)

10

until

11

(

12

(d == l_v)

13

and

14

nexttime (c != l_v)

15

)

16

);

17

endproperty

18

Fig. 16.11 Property illustrating local variable flow

PF10 If v flows into disable iff ( b ) p, then v flows into p. Analogous rules
apply to accept_on , reject_on , sync_accept_on , and sync_reject_on .

As an example of analyzing local variable flow using these rules, consider the
property in Fig. 16.11 .ByRule DF , l_v does not flow into Line 3 .ByRule IF4 ,
l_v flows out of Line 4 , and so by Rule IF7 , l_v flows out of Line 7 .Rule PF4 then
says that l_v flows into Line 9 , and so by Rule PF8 , l_v flows into both Line 10
and Line 12 . This implies that the reference to l_v in Line 10 is legal. By Rule PF3 ,
l_v flows into both Line 13 and Line 15 . This implies that the reference to l_v in
Line 13 is legal. Finally, by Rule PF6 , l_v flows into the expression c!=l_v ,so
the reference to l_v in Line 15 is also legal.

16.4.2 Becoming Unassigned

Once assigned, local variables only become unassigned upon match of subsequences
formed from certain sequence operators. Code in which local variables become
unassigned is of poor style and should be avoided.
Figure 16.12 shows an example in which the local variable l_v becomes
unassigned upon match of an and subsequence. The semantics of the and sequence
operator requires the subevaluations of the operands to join together once both
have matched. This requires all local variables that are assigned to have consistent,
unambiguous values in the continuing thread of evaluation. There are assignments
to l_v in both operands of the and (Lines 4 and 6 ), so l_v may not have a single