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

IF4 v flows out of ( r , v = e ) .If w flows into ( r , v = e ) , then w flows into r .
w flows out of ( r , v = e ) iff w flows out of r .Ife references w , then w must
flow out of r .
IF5 If v flows into r ## ns, then v flows into r .If v flows out of r , then v flows
across ## n into s. v flows out of r ## nsiff v flows out of s. Analogous
rules apply to the variants of the binary concatenation operator. The flow rules
for unary concatenation are obtained from those for binary concatenation by
replacing r with 1'b1 .
IF6 If v flows into r or s, then v flows into both r and s. v flows out of r or s
iff v flows out of both r and s.
IF7 If v flows into r and s, then v flows into both r and s. v flows out of r and s
iff either v flows out of r and there is no assignment to v in s or v flows out of
s and there is no assignment to v in r . Analogous rules apply to intersect
and within .
IF8 If v flows into b throughout r , then v flows into both b and r . v flows out
of b throughout r iff v flows out of r .
IF9 If v flows into first_match ( r ) , then v flows into r . v flows out of
first_match ( r ) iff v flows out of r .
IF10 v flows out of r [ * 0] iff v flows into r [ * 0] .Thevalueof v does not change as
a result of empty match of r [ * 0] .
IF11 If v flows into r [ * n ] , where n is positive, then v flows into the first iteration
of r . v flows out of r [ * n ] iff v flows out of r , in which case v flows into and
out of each iteration of r .If v does not flow out of r , then v does not flow into
any iteration of r after the first. Analogous rules apply to ranged forms of the
repetition operator. If the lower range is zero, then the flow rule is obtained by
decomposing r [ * 0: n ] as r [ * 0] or r [ * 1: n ] (n positive or $ ).
PF1 If v flows into strong ( r ) , then v flows into r . An analogous rule applies to
weak .
PF2 If v flows into not p, then v flows into p.
PF3 If v flows into p or q, then v flows into both p and q. Analogous rules apply
to and , implies , and iff .
PF4 If v flows into r |-> p, then v flows into r .If v flows out of r , then v flows
across |-> and into p. Analogous rules apply to |=> , #-# , and #=# .
PF5 If v flows into if ( b ) p else q, then v flows into b, p, and q. An analogous
rule applies to case .
PF6 If v flows into nexttime p, then v flows into p. Analogous rules apply to
s_nexttime and to the indexed forms of these operators.
PF7 If v flows into always p, then v flows into p. Analogous rules apply to
s_always and to the ranged forms of these operators.
PF8 If v flows into p until q, then v flows into both p and q. Analogous rules
apply to s_until , until_with , and s_until_with .
PF9 If v flows into s_eventually p, then v flows into p. Analogous rules apply
to the ranged form of this and the weak eventually operator.