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

￿ w ;L 0 ;L 1 j b iff j w jD 1 and w 0

ˆ bŒL 0 and L 1 D L 0 . Here, bŒL 0 denotes
the expression obtained by substituting values from L 0 for any references in b to

local variables in dom.L 0 /.
￿ w ;L 0 ;L 1 j ( r , v = e ) iff there exists L such that w ;L 0 ;L j r and L 1 D
L n v [f v ;eŒL; w 0 g . Here, eŒL; w 0 denotes the expression obtained by substituting
values from L 0 for any references in e to local variables in dom.L 0 / and then
using values from w 0 to evaluate remaining references in e.If w 0 is a special
letter > or ? , then eŒL; w 0 can be any value.
￿ w ;L 0 ;L 1 j r ##1 s iff there exist x; y; L such that w D xy and x; L 0 ;L j r
and y; L; L 1 j s.
￿ w ;L 0 ;L 1 j r ##0 s iff there exist x; y; z ;L such that w D xy z and j y jD 1
and xy; L 0 ;L j r and y z ;L;L 1 j s.
￿ w ;L 0 ;L 1 j r or s iff there exists L such that both
- either w ;L 0 ;L j r or w ;L 0 ;L j s, and
- L 1 D L j D , where D D flow . dom .L 0 /; r or s/.
￿ w ;L 0 ;L 1 j r intersect s iff there exist L; L 0 such that w ;L 0 ;L j r and
w ;L 0 ;L 0 j s and L 1 D L j D [ L 0 j D 0 , where
- D D flow .dom.L 0 /; r/ assign .s/
- D 0 D flow .dom.L 0 /; s/ assign .r/
￿ w ;L 0 ;L 1 j first_match ( r ) iff both
- w ;L 0 ;L 1 j r , and
- if there exist x; y; L such that w D xy and N x; L 0 ;L j r , then y is empty.
￿ w ;L 0 ;L 1 j r [ * 0] iff j w jD 0 and L 1 D L 0 .
￿ w ;L 0 ;L 1 j r [+] iff there exist L .0/ D L 0 ; w 1 ;L .1/ ;:::; w k ;L .k/ D L 1 , k 1,
such that w D w 1 w k and w i ;L .i 1/ ;L .i / j r for every i , 1 i k.

22.6.4 Property Semantics with Local Variables

Local variables do not flow out of properties, so the semantics of property
satisfaction with local variables is simpler than that of sequence matching. The
relation is three-way:

w ;L 0 ˆ p

The relation holds if p is satisfied by word w starting with the incoming local
variable context L 0 . Here are the definitions for the basic property operators:
￿ w ;L 0 ˆ not p iff N w ;L 0 6ˆ p.
￿ w ;L 0 ˆ strong ( r ) iff there exists 0 j< j w j and L such that
w 0;j ;L 0 ;L j r . r must not admit an empty match.