Formal Semantics - SVA: The Power of Assertions in SystemVerilog - page 492

The “disabled” disposition of a disable iff is defined formally as follows:
w ˆ

d

disable iff ( b ) p

for some i , w i

iff ˆ b, and for the least such i , both

w 0;i 1

!

> ˆ p

and

w 0;i 1

!

6ˆ p.
Intuitively, the requirement that w 0;i 1

?

!

ˆ p ensures that p has not failed prior to
the occurrence of the disable condition, while the requirement that w 0;i 1

>

!

6ˆ p
ensures that p has not succeeded prior to the occurrence of the disable condition.

?

22.6 Formal Semantics of Local Variables

This section gives an overview of the formal semantics of local variables. For
more details, see the LRM [ 8 ]. The technical report [ 41 ] is another good reference,
covering details of theoretical results that are not presented in the LRM. [ 23 ]
presents complexity results for local variables. Only the unclocked semantics is
discussed here. As usual, the clocked semantics is obtained by first transforming
to unclocked forms using the clock rewrite rules and then applying the unclocked
semantics.

22.6.1 Formalizing Local Variable Flow

If X is a set of local variables and r is a sequence, let flow .X; r/ denote the set
of local variables that flow out of r given that the local variables in X flow into r .
From the local variable flow rules in Sect. 16.4.1 , one obtains the following recursive
representation of flow .X; r/:

SF1 flow .X; b/ D X . Analogous equalities hold for Boolean repetitions b [-> n ] ,
b [= n ] ,etc.
SF2 flow .X; ( r , v = e ) / D flow .X; r/ [f v g .
SF3 flow .X; r ## ns/ D flow . flow .X; r/; s/. Analogous equalities hold for vari-
ants of the binary concatenation operator.
SF4 flow .X; r or s/ D flow .X; r/ \ flow .X; s/.
SF5 flow .X; r and s/ D . flow .X; r/ assign .s// [ . flow .X; s/ assign .r//.
Here assign .r/ (resp., assign .s/) denotes the set of local variables assigned
anywhere within r (resp., s). Analogous equalities hold for intersect and
within .
SF6 flow .X; b throughout r/ D flow .X; r/.
SF7 flow .X; first_match ( r ) / D flow .X; r/.
SF8 flow .X; r [ * 0] / D X .