Subject: [sv-ac] mapping SVA2PSL, first draft
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Apr 30 2003 - 17:33:12 PDT
All:
Below is a draft of a SVA2PSL mapping.
The mapping domain does not include local variables
or first_match. Also, clocked SVA sequences are in
the domain of the mapping only if they are not tightly
satisfied by emptyword.
The semantic claims do not cover the abort operator,
as the PSL abort is not yet "fixed". Also, the
semantic claims for properties and assertions do
not apply to finite words because the finite word
semantics of SVA is written with strong and weak
satisfactions, while the finite word semantics for
PSL is written with a neutral satisfaction.
I think this draft is a good starting point for work
on the SVA/PSL alignment.
Note that I have not said anything about how SVA derived
forms are mapped. Of course, they must map consistently
with their definitions in terms of the basic forms. The
derived operators must not be overlooked in the SVA/PSL
alignment.
Best regards,
John Havlicek
===========================================================================
MAPPING SVA TO PSL
===========================================================================
SVA Abstract Syntax
-------------------
Note that local variables and first_match are not in the domain of the
mapping. Throughout, "unclocked SVA sequence" means "unclocked SVA sequence
without local variables or first_match". Similarly, "clocked SVA sequence"
means "clocked SVA sequence without local variables or first_match".
The abstract grammar for unclocked SVA sequences is
R ::= b
| (R)
| (R ##1 R)
| (R ##0 R)
| (R or R)
| (R intersect R)
| R[*0]
| R[*1:$]
The abstract grammar for clocked SVA sequences is
S ::= @(b) R
| (S ## S)
The abstract grammar for unclocked SVA properties is
P ::= [disable iff (b)] [not] R
| [disable iff (b)] [not] (R |-> [not] R)
Note: In this grammar, "[...]" denotes an optional component.
The abstract grammar for clocked SVA properties is
Q ::= @(b) P
| [disable iff (b)] [not] S
| [disable iff (b)] [not] (S |-> [not] S)
Note: In this grammar, "[...]" denotes an optional component.
The abstract grammar for SVA assertions is
A ::= always assert property Q
| always @(b) assert property P
| initial assert property Q
| initial @(b) assert property P
===========================================================================
MAPPING DEFINITION
===========================================================================
1. Mapping unclocked SVA sequences to PSL unclocked SEREs
---------------------------------------------------------
DEFINITION 1: Let b be a boolean expression, and let
R, R_1, R_2 be unclocked SVA sequences.
* M(b) = b
* M((R)) = {M(R)}
* M((R_1 ##1 R_2)) = {M(R_1) ; M(R_2)}
* M((R_1 ##0 R_2)) = {M(R_1) : M(R_2)}
* M((R_1 or R_2)) = {{M(R_1)} | {M(R_2)}}
* M((R_1 intersect R_2)) = {{M(R_1)} && {M(R_2)}}
* M(R[*0]) = 1[*0]
* M(R[*1:$]) = M(R)[*1:]
////
REMARK: Note that the PSL LRM, Verilog flavor is supposed to use ":"
instead of "..". This is why I have written "[*1:]" rather than
"[*1..]".
////
PROPOSITION 1.1: Let r be an unclocked SVA sequence and let w be a finite
word over 2^P. Then w |== r iff w |= M(r).
PROOF: By induction over the structure of r.
* r = b.
w |== b
iff |w| = 1 and w^0 |= b
iff |w| = 1 and w^0 |= M(b)
iff w |= M(b)
* r = (R).
w |== (R)
iff w |== R
iff [induction]
w |= M(R)
iff w |= {M(R)}
iff w |= M((R))
* r = (R_1 ##1 R_2).
w |== (R_1 ##1 R_2)
iff there exist x,y such that w = xy and x |== R_1 and y |== R_2
iff [induction]
there exist x,y such that w = xy and x |= M(R_1) and y |= M(R_2)
iff w |= M(R_1) ; M(R_2)
iff w |= {M(R_1) ; M(R_2)}
iff w |= M((R_1 ##1 R_2))
* r = (R_1 ##0 R_2).
w |== (R_1 ##0 R_2)
iff there exist x,y,z such that w = xyz and |y| = 1 and xy |== R_1 and yz |== R_2
iff [induction]
there exist x,y such that w = xyz and |y| = 1 and xy |= M(R_1) and yz |= M(R_2)
iff w |= M(R_1) : M(R_2)
iff w |= {M(R_1) : M(R_2)}
iff w |= M((R_1 ##0 R_2))
* r = (R_1 or R_2).
w |== (R_1 or R_2)
iff w |== R_1 or w |== R_2
iff [induction]
w |= M(R_1) or w |= M(R_2)
iff w |= {M(R_1)} | {M(R_2)}
iff w |= {{M(R_1)} | {M(R_2)}}
iff w |= M((R_1 or R_2))
* r = (R_1 intersect R_2).
w |== (R_1 intersect R_2)
iff w |== R_1 andr w |== R_2
iff [induction]
w |= M(R_1) and w |= M(R_2)
iff w |= {M(R_1)} && {M(R_2)}
iff w |= {{M(R_1)} && {M(R_2)}}
iff w |= M((R_1 intersect R_2))
* r = R[*0].
w |= M(R[*0])
iff w |= 1[*0]
iff w |= FALSE[*]
iff |w| = 0 or there exist w_1,...,w_j such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |= FALSE
iff [Since w is over 2^P, w = w_1...w_j implies not(w_1 |= FALSE)]
|w| = 0
iff w |== R[*0]
* r = R[*1:$].
w |== R[*1:$]
iff there exist w_1,...,w_j, j >= 1, such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |== R
iff [induction]
there exist w_1,...,w_j, j >= 1, such that w = w_1...w_j and for each
i such that 1 <= i <= j, w_i |= M(R)
iff there exist w_1,y such that w = w_1y and w_1 |= M(R) and either
y is empty or there exist w_2,...,w_j such that y = w_2...w_j and
for each i such that 2 <= i <= j, w_i |= M(R)
iff there exist w_1, y such that w = w_1y and w_1 |= M(R) and y |= M(R)[*]
iff w |= {M(R);M(R)[*]}
iff w |= M(R)[*1:]
iff w |= M(R[*1:$])
////
REMARK: In PSL, "TRUE" means "p || !p" and "FALSE" means "p && !p" for
some choice of atomic proposition p. In SVA, "\top" satisfies all
boolean expressions, while "\bot" satisfies no boolean expression. In
particular, \top |= FALSE. As a result, Proposition 1 does not hold
for words w over 2^P \cup {\top, \bot}. For example, if w is the
length 1 word with w^0 = \top, then
not(w |== 1[*0])
but
w |= FALSE[*], hence w |= M(1[*0])
////
===========================================================================
2. Mapping clocked SVA sequences to PSL clocked SEREs
-----------------------------------------------------
NOTATION: If S is a clocked SVA sequence, let <S> denote
the unclocked SVA sequence that results from S by applying the
SVA clock rewrite rules.
////
PROPOSITION 2.1: Let r be an unclocked SVA sequence, and let w be a
finite word over 2^P. Then the following are equivalent:
1. w |== <@(c) r> .
2. w |=(c) M(r) .
PROOF: By induction over the structure of r.
* r = b.
w |== <@(c) b>
iff w |== (!c[*0:$] ##1 c & b)
iff |w| >= 1 and for every i s.t. 0 <= i < |w| - 1, w^i |= !c and
w^{|w|-1} |= c & b
iff w |=(c) b
iff w |=(c) M(b)
* r = (R).
w |== <@(c) (R)>
iff w |== <@(c) R>
iff [induction]
w |=(c) M(R)
iff w |=(c) {M(R)}
iff w |=(c) M((R))
* r = (R_1 ##1 R_2).
w |== <@(c) (R_1 ##1 R_2)>
iff w |== (<@(c) R_1> ##1 <@(c) R_2>)
iff there exist x,y such that w = xy and x |== <@(c) R_1> and y |== <@(c) R_2>
iff [induction]
there exist x,y such that w = xy and x |=(c) M(R_1) and y |=(c) M(R_2)
iff w |=(c) M(R_1) ; M(R_2)
iff w |=(c) {M(R_1) ; M(R_2)}
iff w |=(c) M((R_1 ##1 R_2))
* r = (R_1 ##0 R_2).
w |== <@(c) (R_1 ##0 R_2)>
iff w |== (<@(c) R_1> ##0 <@(c) R_2>)
iff there exist x,y,z such that w = xyz and |y| = 1 and xy |== <@(c) R_1>
and yz |== <@(c) R_2>
iff [induction]
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(c) M(R_1)
and yz |=(c) M(R_2)
iff w |=(c) M(R_1) : M(R_2)
iff w |=(c) {M(R_1) : M(R_2)}
iff w |=(c) M((R_1 ##0 R_2))
* r = (R_1 or R_2).
w |== <@(c) (R_1 or R_2)>
iff w |== (<@(c) R_1> or <@(c) R_2>)
iff w |== <@(c) R_1> or w |== <@(c) R_2>
iff [induction]
w |=(c) M(R_1) or w |=(c) M(R_2)
iff w |=(c) {M(R_1)} | {M(R_2)}
iff w |=(c) {{M(R_1)} | {M(R_2)}}
iff w |=(c) M((R_1 or R_2))
* r = (R_1 intersect R_2).
w |== <@(c) (R_1 intersect R_2)>
iff w |== (<@(c) R_1> intersect <@(c) R_2>)
iff w |== <@(c) R_1> and w |== <@(c) R_2>
iff [induction]
w |=(c) M(R_1) and w |=(c) M(R_2)
iff w |=(c) {M(R_1)} && {M(R_2)}
iff w |=(c) {{M(R_1)} && {M(R_2)}}
iff w |=(c) M((R_1 intersect R_2))
* r = R[*0].
w |== <@(c) R[*0]>
iff w |== (<@(c) R>)[*0]
iff |w| = 0
iff [Since w is over 2^P, w = w_1...w_j implies not(w_1 |= FALSE)]
|w| = 0 or there exist w_1,...,w_j such that w = w_1...w_j and for all
i such that 1 <= i <= j, w_i |=(c) FALSE
iff w |=(c) FALSE[*]
iff w |=(c) 1[*0]
iff w |=(c) M(R[*0])
* r = R[*1:$].
w |== <@(c) R[*1:$]>
iff w |== (<@(c) R>) [*1:$]
iff there exist w_1,...,w_j such that w = w_1...w_j and for all i such that
1 <= i <= j, w_i |== <@(c) R>
iff [induction]
there exist w_1,...,w_j such that w = w_1...w_j and for all i such that
1 <= i <= j, w_i |=(c) M(R)
iff there exist w_1,y such that w = w_1y and w_1 |=(c) M(R) and either
y is empty or there exist w_2,...,w_j such that y = w_2...w_j and
for each i such that 2 <= i <= j, w_i |=(c) M(R)
iff there exist w_1, y such that w = w_1y and w_1 |=(c) M(R) and y |=(c) M(R)[*]
iff w |=(c) {M(R);M(R)[*]}
iff w |=(c) M(R)[*1:]
iff w |=(c) M(R[*1:$])
////
LEMMA 2.1: Let w be a non-empty word over 2^P and let r be an unclocked SERE.
Then w |=(c) r iff w |=(TRUE) {r}@c.
PROOF: By induction over the structure of r. If no letter of w satisfies
c then let I = |w|. Otherwise, let I be the smallest non-negative integer
such that w^I |= c.
* r = b.
w |=(TRUE) {b}@c
iff I < |w| and w^{I..} |=(c) {b}
iff I < |w| and w^{I..} |=(c) b
iff I = |w|-1 and w^I |= c & b
iff w |=(c) b
* r = {R}.
w |=(c) {R}
iff w |=(c) R
iff [induction]
w |=(TRUE) R@c
iff I < |w| and w^{I..} |=(c) R
iff I < |w| and w^{I..} |=(c) {R}
iff I < |w| and w^{I..} |=(c) {{R}}
iff w |=(TRUE) {{R}}@c
* r = R_1 ; R_2.
w |=(c) R_1 ; R_2
iff A:
there exist x,y such that w = xy and x |=(c) R_1 and y |=(c) R_2
w |=(TRUE) {R_1 ; R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1 ; R_2}
iff I < |w| and w^{I..} |=(c) R_1 ; R_2
iff B:
I < |w| and there exist x',y' such that w^{I..} = x'y' and x' |=(c) R_1
and y' |=(c) R_2
Assume A. Since w is non-empty, either x or y is non-empty.
Suppose x is non-empty. Then
[induction]
there exist x non-empty, y such that w = xy and x |=(TRUE) {R_1}@c
and y |=(c) R_2
=> there exist x non-empty, y such that w = xy and I < |x| and
x^{I..} |=(c) R_1 and y |=(c) R_2
=> [x' = x^{I..}, y' = y]
B
Suppose x is empty and y is non-empty. Then
[induction]
there exist x empty, y non-empty such that w = xy and x |=(c) R_1
and y |=(TRUE) {R_2}@(c)
=> there exist x empty, y non-empty such that w = xy and x |=(c) R_1
and I < |y| and y^{I..} |=(c) R_2
=> [x' is empty, y' = y^{I..}]
B
Now assume B. Since I < |w|, w^{I..} is non-empty, hence either x' or y'
is non-empty. Suppose x' is non-empty. Then
I < |w| and there exist x' non-empty, y' such that w^{I..} = x'y' and
x' |=(c) {R_1} and y' |=(c) R_2
=> [x' non-empty and w^{I..} = x'y' imply that x' = {w^{0,I-1}x'}^{I..}]
there exist x' non-empty, y' such that w^{I..} = x'y' and
w^{0,I-1}x' |=(TRUE) {R_1}@c and y' |=(c) R_2
=> [induction]
there exist x' non-empty, y' such that w^{I..} = x'y' and
w^{0,I-1}x' |=(c) R_1 and y' |=(c) R_2
=> [x = w^{0,I-1}x', y = y']
A
Suppose x' is empty and y' is non-empty. Then
I < |w| and there exist x' empty, y' non-empty such that w^{I..} = x'y'
and x' |=(c) R_1 and y' |=(c) {R_2}
=> [x' empty and y' non-empty and w^{I..} = x'y' imply that
y' = {w^{0,I-1}y'}^{I..}]
there exist x' empty, y' non-empty such that w^{I..} = x'y' and
x' |=(c) R_1 and w^{0,I-1}y' |=(TRUE) {R_2}@c
=> [induction]
there exist x' empty, y' non-empty such that w^{I..} = x'y' and
x' |=(c) R_1 and w^{0,I-1}y' |=(c) R_2
=> [x = empty, y = xy = w = w^{0,I-1}y']
A
* r = R_1 : R_2.
w |=(c) R_1 : R_2
iff A:
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(c) R_1
and yz |=(c) R_2
w |=(TRUE) {R_1 : R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1 : R_2}
iff I < |w| and w^{I..} |=(c) R_1 : R_2
iff B:
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and x'y' |=(c) R_1 and y'z' |=(c) R_2
Assume A. Then
[induction]
there exist x,y,z such that w = xyz and |y| = 1 and xy |=(TRUE) {R_1}@c
and yz |=(c) R_2
=> there exist x,y,z such that w = xyz and |y| = 1 and
I < |xy| and {xy}^{I..} |=(c) R_1 and yz |=(c) R_2
=> [I < |xy| implies {xy}^{I..} = x'y; let y' = y, z' = z]
B
Assume B. Then
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and x'y' |=(c) {R_1} and y'z' |=(c) R_2
=> [x'y' = {w^{0,I-1}x'y'}^{I..}]
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and w^{0,I-1}x'y' |=(TRUE) {R_1}@c and y'z' |=(c) R_2
=> [induction]
I < |w| and there exist x',y',z' such that w^{I..} = x'y'z' and |y'| = 1
and w^{0,I-1}x'y' |=(c) R_1 and y'z' |=(c) R_2
=> [x = w^{0,I-1}x', y = y', z = z']
A
* r = {R_1} | {R_2}.
w |=(c) {R_1} | {R_2}
iff w |=(c) R_1 or w |=(c) R_2
iff [induction]
w |=(TRUE) {R_1}@c or w |=(TRUE) {R_2}@c
iff I < |w| and either w^{I..} |=(c) {R_1} or w^{I..} |=(c) {R_2}
iff I < |w| and either w^{I..} |=(c) R_1 or w^{I..} |=(c) R_2
iff I < |w| and w^{I..} |=(c) {R_1} | {R_2}
iff I < |w| and w^{I..} |=(c) {{R_1} | {R_2}}
iff w |=(TRUE) {{R_1} | {R_2}}@c
* r = {R_1} && {R_2}.
w |=(c) {R_1} && {R_2}
iff w |=(c) R_1 and w |=(c) R_2
iff [induction]
w |=(TRUE) {R_1}@c and w |=(TRUE) {R_2}@c
iff I < |w| and w^{I..} |=(c) {R_1} and w^{I..} |=(c) {R_2}
iff I < |w| and w^{I..} |=(c) R_1 and w^{I..} |=(c) R_2
iff I < |w| and w^{I..} |=(c) {R_1} && {R_2}
iff I < |w| and w^{I..} |=(c) {{R_1} && {R_2}}
iff w |=(TRUE) {{R_1} && {R_2}}@c
* r = R[*].
w |=(TRUE) {R[*]}@c
iff I < |w| and w^{I..} |=(c) {R[*]}
iff I < |w| and w^{I..} |=(c) R[*]
iff [w^{I..} is non-empty]
I < |w| and there exist u_1,...,u_j non-empty such that
w^{I..} = u_1,...,u_k and for each i such that 1 <= i <= j,
u_i |=(c) R
iff I < |w| and there exist u_1,...,u_j non-empty such that
w^{I..} = u_1,...,u_j and u_1 |=(c) {R} and for each i such
that 1 < i <= j, u_i |=(c) R
iff [u_1 = {w^{0,I-1}u_1}^{I..}]
there exist u_1,...,u_j non-empty such that
w = w^{0,I-1}u_1...u_j and w^{0,I-1}u_1 |=(TRUE) {R}@c and
for each i such that 1 < i <= j, u_i |=(c) R
iff [induction]
there exist u_1,...,u_j non-empty such that
w = w^{0,I-1}u_1...u_j and w^{0,I-1}u_1 |=(c) R and
for each i such that 1 < i <= j, u_i |=(c) R
iff [w_1 = w^{0,I-1}u_1, w_i = u_i for 1 < i <= j]
there exist w_1,...,w_j non-empty such that w = w_1...w_j and
for each i such that 1 <= i <= j, w_i |=(c) R
iff [w is non-empty]
w |=(c) R[*]
////
REMARK: Lemma 2.1 fails if w is empty. For example, emptyword |=(c) 1[*0],
but not(emptyword |=(TRUE) {1*[0]}@c).
////
PROPOSITION 2.2: Let r be an unclocked SVA sequence and let w be a
non-empty finite word over 2^P. Then the following are equivalent:
1. w |== <@(c) r> .
2. w |=(c) M(r) .
3. w |=(TRUE) {M(r)}@c .
PROOF: 1 and 2 are equivalent by Proposition 2.1. Since w is
non-empty, Lemma 2.1 shows that 2 and 3 are equivalent.
////
DISCUSSION: The breakdown of Lemma 2.1, hence the equivalence of
2 and 3 in Proposition 2.2, when w is empty indicates that some care
is required in defining the mapping on clocked SVA sequences.
Naively, the definition should be
* M(@(b) R) = {M(R)} @b
* M((S_1 ## S_2)) = {M(S_1) ; M(S_2)}
but this will lead to problems if, e.g., emptyword tightly satisfies
one or both of <S_1>, <S_2>. The domain of the mapping will be
restricted to avoid these problems.
////
DEFINITION 2: Let b be a boolean expression, let R be an unclocked SVA
sequence, and let S_1, S_2 be clocked SVA sequences.
* If emptyword does not tightly satisfy R, then M(@(b) R) = {M(R)} @b.
Otherwise, @(b) R is not in the domain of M.
* If both S_1 and S_2 are in the domain of M, then
M((S_1 ## S_2)) = {M(S_1) ; M(S_2)}. Otherwise, (S_1 ## S_2) is not
in the domain of M.
////
LEMMA 2.2: If c is a boolean expression and r is an unclocked SVA
sequence, then emptyword tightly satisfies <@(c) r> iff
emptyword tightly satisfies r.
PROOF: By induction over the structure of r. Write e for emptyword.
* r = b.
e does not tightly satisfy b. <@(c) b> = (!c[*0:$];c&b), which is
also not tightly satisfied by b.
* r = (R).
e |== (R)
iff e |== R
iff [induction]
e |== <@(c) R>
iff e |== <@(c) (R)>
* r = (R_1 ##1 R_2).
e |== (R_1 ##1 R_2)
iff e |== R_1 and e |== R_2
iff [induction]
e |== <@(c) R_1> and e |== <@(c) R_2>
iff e |== (<@(c) R_1> ##1 <@(c) R_2>)
iff e |== <@(c)(R_1 ##1 R_2)>
* r = (R_1 ##0 R_2).
e does not tightly satisfy (R_1 ##0 R_2).
<@(c)(R_1 ##0 R_2)> = (<@(c) R_1> ##0 <@(c) R_2>), which is also not
tightly satisfied by e.
* r = (R_1 or R_2).
e |== (R_1 or R_2)
iff e |== R_1 or e |== R_2
iff [induction]
e |== <@(c) R_1> or e |== <@(c) R_2>
iff e |== (<@(c) R_1> or <@(c) R_2>)
iff e |== <@(c)(R_1 or R_2)>
* r = (R_1 intersect R_2).
e |== (R_1 intersect R_2)
iff e |== R_1 and e |== R_2
iff [induction]
e |== <@(c) R_1> and e |== <@(c) R_2>
iff e |== (<@(c) R_1> intersect <@(c) R_2>)
iff e |== <@(c)(R_1 intersect R_2)>
* r = R[*0].
e |== R[*0]. <@(c) R[*0]> = (<@(c) R>)[*0], which is also tightly
satisfied by e.
* r = R[*1:$].
e |== R[*1:$]
iff e |== R
iff [induction]
e |== <@(c) R>
iff e |== (<@(c) R>)[*1:$]
iff e |== <@(c) R[*1:$]>
////
LEMMA 2.3: If s is a clocked SVA sequence in the domain of M, then
emptyword does not tightly satisfy <s>.
PROOF: By induction over the structure of s.
* s = @(b) R. By definition, emptyword does not tightly satisfy R.
By Lemma 2.2, emptyword does not tightly satisfy <s>.
* s = (S_1 ## S_2). By definition, S_1 and S_2 are both in the domain
of M. By induction, emptyword tightly satisfies neither <S_1> nor
<S_2>. <s> = (<S_1> ##1 <S_2>), so it follows that emptyword does
not tightly satisfy <s>.
////
PROPOSITION 2.3: Let s be a clocked SVA sequence in the domain of M,
and let w be a non-empty finite word over 2^P. Then the following are
equivalent:
1. w |== <s> .
2. w |=(TRUE) M(s) .
PROOF: By induction over the structure of s.
* s = @(c) R. The result follows from Proposition 2.2.
* s = (S_1 ## S_2). Then both S_1, S_2 are in the domain of M.
By Lemma 2.3, emptyword tightly satisfies neither <S_1> nor <S_2>.
w |== <(S_1 ## S_2)>
iff w |== (<S_1> ##1 <S_2>)
iff there exist x,y such that w = xy and x |== <S_1>
and y |== <S_2>
iff [induction; x,y must be non-empty]
there exist x,y such that w = xy and x |=(TRUE) M(S_1)
and y |=(TRUE) M(S_2)
iff w |=(TRUE) {M(S_1) ; M(S_2)}
iff w |=(TRUE) M((S_1 ## S_2))
////
===========================================================================
3. Mapping unclocked SVA properties to unclocked PSL formulas
-------------------------------------------------------------
Since sequences can be properties, the letter "T" will
be used instead of "M" to denote the mapping at the level
of properties and assertions.
If phi is an unclocked SVA property and if "disable iff (b) phi"
is also an unclocked SVA property, then phi will be called a
"unclocked SVA property fragment".
DEFINITION 3: Let b be a boolean expression, let R, R_1, R_2 be
unclocked SVA sequences, and let phi be an unclocked SVA property
fragment.
* T(R) = {1} |-> {M(R)}!
* T(not R) = !T(R)
* T((R_1 |-> R_2)) = {M(R_1)} |-> {M(R_2)}!
* T(not(R_1 |-> R_2)) = !T((R_1 |-> R_2))
* T((R_1 |-> not R_2)) = {M(R_1)}(!({1} |-> {M(R_2)}!))
* T(not(R_1 |-> not R_2)) = !T((R_1 |-> not R_2))
* T(disable iff (b) phi) = T(phi) abort b
////
NOTATION: For clarity, property satisfaction in SVA is
denoted "|=", while unclocked formula satisfaction in PSL is
denoted "|=.".
////
LEMMA 3.1: Let r be an unclocked SERE, and let w be a
word over 2^P. Then the following are equivalent
1. w |=. {1} |-> {r}! .
2. w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |= r .
PROOF:
w |=. {1} |-> {r}!
iff for every i such that 0 <= i < |w|, if w^{0,i} |= 1,
then there exists j such that i <= j < |w| and w^{i,j} |= r
iff [w^{0,i} |= 1 iff i = 0 and w is non-empty]
w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |= r
////
PROPOSITION 3.1: Let phi be an unclocked SVA property fragment,
and let w be an infinite word over 2^P. Then the following
are equivalent:
1. w |= phi .
2. w |=. T(phi) .
PROOF:
* phi = R.
w |= R
iff there exists j >= 0 such that w^{0,j} |== R
iff [Proposition 1.1]
there exists j >= 0 such that w^{0,j} |= M(R)
iff [Lemma 3.1; w^{0,j} is non-empty]
w |=. {1} |-> {M(R)}!
iff w |=. T(R)
* phi = not R.
w |= not R
iff [\bar w = w]
not(w |= R)
iff [proof for phi = R]
not(w |=. T(R))
iff w |=. !T(R)
iff w |=. T(not R)
* phi = (R_1 |-> R_2).
w |= (R_1 |-> R_2)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== R_1, w^{j..} |= R_2
iff for every j >= 0 such that w^{0,j} |== R_1, there exists k >= j
such that w^{j,k} |== R_2
iff [Proposition 1.1]
for every j >= 0 such that w^{0,j} |= M(R_1), there exists k >= j
such that w^{j,k} |= M(R_2)
iff w |=. {M(R_1)} |-> {M(R_2)}!
iff w |=. T((R_1 |-> R_2))
* phi = not(R_1 |-> R_2).
w |= not(R_1 |-> R_2)
iff [\bar w = w]
not(w |= (R_1 |-> R_2))
iff [proof for phi = (R_1 |-> R_2)]
not(w |=. T((R_1 |-> R_2)))
iff w |=. !T((R_1 |-> R_2))
iff w |=. T(not(R_1 |-> R_2))
* phi = (R_1 |-> not R_2).
w |= (R_1 |-> not R_2)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== R_1, w^{j..} |= not R_2
iff [Proposition 1.1, proof for phi = not R]
for every j >= 0 such that w^{0,j} |= M(R_1),
w^{j..} |= !({1} |-> {M(R_2)}!)
iff w |=. {M(R_1)}(!({1} |-> {M(R_2)}!))
iff w |=. T((R_1 |-> not R_2))
* phi = not(R_1 |-> not R_2).
w |= not(R_1 |-> not R_2)
iff [\bar w = w]
not(w |= (R_1 |-> not R_2))
iff [proof for phi = (R_1 |-> not R_2)]
not(w |=. T((R_1 |-> not R_2)))
iff w |=. !T((R_1 |-> not R_2))
iff w |=. T(not(R_1 |-> not R_2))
////
REMARK: The PSL semantics for abort needs to be updated before
Proposition 3.1 can be extended to general unclocked SVA properties.
Also, the semantic characterization of the mapping on finite
words requires reconciliation of the finite semantics for SVA and
PSL. Currently, SVA has no neutral semantics for finite words, while
PSL does not yet have strong and weak finite word semantics.
////
===========================================================================
4. Mapping clocked SVA properties to PSL formulas
-------------------------------------------------
Since sequences can be properties, the letter "T" will
be used instead of "M" to denote the mapping at the level
of properties and assertions.
If psi is a clocked SVA property and if "disable iff (b) psi"
is also a clocked SVA property, then psi will be called a
"clocked SVA property fragment".
DISCUSSION: Some care is needed in defining the mapping
for clocked SVA properties, since the form of the property
determines whether strong or weak clocks are needed in PSL.
The mapping is defined following the SVA clock rewrite rules
in order to ensure proper semantic correspondence.
////
DEFINITION 4: Let b,c be boolean expression, let R, R_1, R_2
be unclocked SVA sequences, let phi be an unclocked SVA property
fragment, let S, S_1, S_2 be clocked SVA sequences, and let psi
be a clocked SVA property fragment.
* T(S) = {1} |-> {M(S)}!
* T(not S) = !T(S)
* T((S_1 |-> S_2)) = {M(S_1)} |-> {M(S_2)}!
* T(not (S_1 |-> S_2)) = !T((S_1 |-> S_2))
* T((S_1 |-> not S_2)) = {M(S_1)}(!({1} |-> {M(S_2)}!))
* T(not (S_1 |-> not S_2)) = !T((S_1 |-> not S_2))
* T(disable iff (b) psi) = T(psi) abort b
* T(@(c) not b) = T(@(c) !b)
* T(@(c) not R) = !T(@(c) R), provided R is not a boolean expression.
* T(@(c) (R_1 |-> R_2)) = T((@(c) R_1 |-> @(c) R_2))
* T(@(c) not (R_1 |-> R_2)) = !T(@(c) (R_1 |-> R_2))
* T(@(c) (R_1 |-> not b)) = T((@(c) R_1 |-> @(c) !b))
* T(@(c) (R_1 |-> not R_2)) = T((@(c) R_1 |-> not @(c) R_2)),
provided R_2 is not a boolean expression.
* T(@(c) not (R_1 |-> not R_2)) = !T(@(c) (R_1 |-> not R_2))
* T(@(c) disable iff (b) phi) = T(@(c) phi) abort b
It is understood that if the rhs of one of these rules refers,
e.g., to M(S), then S must be in the domain of M in order for
the argument of T on the lhs to be in the domain of T.
////
LEMMA 4.1: Let r be a clocked SERE, and let w be a
word over 2^P. Then the following are equivalent
1. w |=(TRUE) {1} |-> {r}! .
2. w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |=(TRUE) r .
PROOF:
w |=(TRUE) {1} |-> {r}!
iff for every i such that 0 <= i < |w|, if w^{0,i} |=(TRUE) 1,
then there exists j such that i <= j < |w| and w^{i,j} |=(TRUE) r
iff [since w is over 2^P, w^{0,i} |=(TRUE) 1 iff i = 0 and w is non-empty]
w is empty or there exists j such that 0 <= j < |w|
and w^{0,j} |=(TRUE) r
////
PROPOSITION 4.1: Let psi be a clocked SVA property fragment
in the domain of T, and let w be an infinite word over 2^P.
Then the following are equivalent:
1. w |= psi .
2. w |=(TRUE) T(psi) .
PROOF:
* psi = S.
w |= S
iff w |= <S>
iff there exists j >= 0 such that w^{0,j} |== <S>
iff [Proposition 2.3]
there exists j >= 0 such that w^{0,j} |=(TRUE) M(S)
iff [Lemma 4.1; w^{0,j} is non-empty]
w |=(TRUE) {1} |-> {M(S)}!
iff w |=(TRUE) T(S)
* psi = not S.
w |= not S
iff w |= not <S>
iff [\bar w = w]
not(w |= <S>)
iff [proof for psi = S]
not(w |=(TRUE) {1} |-> {M(S)}!)
iff w |=(TRUE) !({1} |-> {M(S)}!)
iff w |=(TRUE) T(not S)
* psi = (S_1 |-> S_2).
w |= (S_1 |-> S_2)
iff w |= (<S_1> |-> <S_2>)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== <S_1>, w^{j..} |= <S_2>
iff for every j >= 0 such that w^{0,j} |== <S_1>, there exists k >= j
such that w^{j,k} |== <S_2>
iff [Proposition 2.3]
for every j >= 0 such that w^{0,j} |=(TRUE) M(S_1), there exists k >= j
such that w^{j,k} |=(TRUE) M(S_2)
iff w |=(TRUE) {M(S_1)} |-> {M(S_2)}!
iff w |=(TRUE) T((S_1 |-> S_2))
* psi = not(S_1 |-> S_2).
w |= not(S_1 |-> S_2)
iff w |= not(<S_1> |-> <S_2>)
iff [\bar w = w]
not(w |= (<S_1> |-> <S_2>))
iff [proof for psi = (S_1 |-> S_2)]
not(w |=(TRUE) T((S_1 |-> S_2)))
iff w |=(TRUE) !T((S_1 |-> S_2))
iff w |=(TRUE) T(not(S_1 |-> S_2))
* psi = (S_1 |-> not S_2).
w |= (S_1 |-> not S_2)
iff w |= (<S_1> |-> not <S_2>)
iff [\bar w = w]
for every j >= 0 such that w^{0,j} |== <S_1>, w^{j..} |= not <S_2>
iff [Proposition 2.3, proof for psi = not S]
for every j >= 0 such that w^{0,j} |= M(S_1),
w^{j..} |= !({1} |-> {M(S_2)}!)
iff w |=(TRUE) {M(S_1)}(!({1} |-> {M(S_2)}!))
iff w |=(TRUE) T((S_1 |-> not S_2))
* psi = not(S_1 |-> not S_2).
w |= not(S_1 |-> not S_2)
iff w |= not(<S_1> |-> not <S_2>)
iff [\bar w = w]
not(w |= (<S_1> |-> not <S_2>))
iff [proof for psi = (S_1 |-> not S_2)]
not(w |=(TRUE) T((S_1 |-> not S_2)))
iff w |=(TRUE) !(T((S_1 |-> not S_2)))
iff w |=(TRUE) T(not(S_1 |-> not S_2))
* psi = @(c) not b.
w |= @(c) not b
iff w |= <@(c) not b>
iff w |= <@(c) !b>
iff [proof for psi = S]
w |=(TRUE) T(@(c) !b)
iff w |=(TRUE) T(@(c) not b)
* psi = @(c) not R, R not a boolean expression.
w |= @(c) not R
iff w |= <@(c) not R>
w |= not <@(c) R>
iff [\bar w = w]
not(w |= <@(c) R>)
iff [proof for psi = S]
not(w |=(TRUE) T(@(c) R))
iff w |=(TRUE) !T(@(c) R)
iff w |=(TRUE) T(@(c) not R)
* psi = @(c) (R_1 |-> R_2)
w |= @(c) (R_1 |-> R_2)
iff w |= <@(c) (R_1 |-> R_2)>
iff w |= (<@(c) R_1> |-> <@(c) R_2>)
iff [proof for psi = (S_1 |-> S_2)]
w |=(TRUE) T((@(c) R_1 |-> @(c) R_2))
iff w |=(TRUE) T(@(c) (R_1 |-> R_2))
* psi = @(c) not (R_1 |-> R_2)
w |= @(c) not (R_1 |-> R_2)
iff w |= <@(c) not (R_1 |-> R_2)>
iff w |= not (<@(c) R_1> |-> <@(c) R_2>)
iff [proof for psi = not (S_1 |-> S_2)]
w |=(TRUE) !T((@(c) R_1 |-> @(c) R_2))
iff w |=(TRUE) T(@(c) not (R_1 |-> R_2))
* psi = @(c) (R_1 |-> not b).
w |= @(c) (R_1 |-> not b)
iff w |= <@(c) (R_1 |-> not b)>
iff w |= (<@(c) R_1> |-> <@(c) !b>)
iff [proof for psi = (S_1 |-> S_2)]
w |=(TRUE) T((@(c) R_1 |-> @(c) !b))
iff w |=(TRUE) T(@(c) (R_1 |-> not b))
* psi = @(c) (R_1 |-> not R_2), R_2 not a boolean expression.
w |= @(c) (R_1 |-> not R_2)
iff w |= <@(c) (R_1 |-> not R_2)>
iff w |= (<@(c) R_1> |-> not <@(c) R_2>)
iff [proof for psi = (S_1 |-> not S_2)]
w |=(TRUE) T((@(c) R_1 |-> not @(c) R_2))
iff w |=(TRUE) T(@(c) (R_1 |-> not R_2))
* psi = @(c) not (R_1 |-> not R_2).
w |= @(c) not (R_1 |-> not R_2)
iff w |= <@(c) not (R_1 |-> not R_2)>
iff w |= not (<@(c) R_1> |-> <@(c) not R_2>)
iff [\bar w = w]
not(w |= (<@(c) R_1> |-> <@(c) not R_2>))
iff not(w |= <@(c) (R_1 |-> not R_2)>)
iff [proofs for psi = @(c) (R_1 |-> not R_2), R_2 boolean and not]
not(w |=(TRUE) T(@(c) (R_1 |-> not R_2)))
iff w |=(TRUE) !T(@(c) (R_1 |-> not R_2))
iff w |=(TRUE) T(@(c) not (R_1 |-> not R_2))
////
REMARK: The PSL semantics for abort needs to be updated before
Proposition 4.1 can be extended to general clocked SVA properties.
Also, the semantic characterization of the mapping on finite
words requires reconciliation of the finite semantics for SVA and
PSL. Currently, SVA has no neutral semantics for finite words, while
PSL does not yet have strong and weak finite word semantics.
////
===========================================================================
5. Mapping SVA assertions to PSL formulas
-----------------------------------------
DEFINITION 5:
* T(always assert property Q) = always T(Q)
* T(always @(b) assert property P) = (always T(P))@b
* T(initial assert property Q) = T(Q)
* T(initial @(b) assert property P) = (T(P))@b
////
LEMMA 5.1: Let f be a PSL formula and let w be an
infinite word over 2^P.
1. w |=(TRUE) always f iff for all i >= 0, w^{i..} |=(TRUE) f.
2. w |=(TRUE) (always f)@b iff for all i >= 0 such that w^i |= b,
w^{i..} |=(b) f
PROOF:
1. w |=(TRUE) always f
iff w |=(TRUE) !(TRUE U !f)
iff not(w |=(TRUE) TRUE U !f)
iff not(there exists k >= 0 such that w^{k..} |=(TRUE) !f and
for all j such that 0 <= j < k, w^{j..} |=(TRUE) TRUE)
iff not(there exists k >= 0 such that w^{k..} |=(TRUE) !f)
iff for all k >= 0, not(w^{k..} |=(TRUE) !f)
iff for all k >= 0, w^{k..} |=(TRUE) f
2. w |=(TRUE) (always f)@b
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then w^{i..} |=(b) always f
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then w^{i..} |=(b) !(TRUE U !f)
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then not(w^{i..} |=(b) TRUE U !f)
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then not(there exists k >= i such that w^k |= b and w^{k..} |=(b) !f
and for all j such that i <= j < k and such that w^j |= b,
w^{j..} |=(b) TRUE)
iff [if w^j |= b, then w^{j..} |=(b) TRUE]
if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then not(there exists k >= i such that w^k |= b and w^{k..} |=(b) !f)
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then for all k >= i such that w^k |= b, not(w^{k..} |=(b) !f)
iff if there exists i >= 0 such that w^{0,i} |=(TRUE) {!b[*];b},
then for all k >= i such that w^k |= b, w^{k..} |=(b) f
iff for all k >= 0 such that w^k |= b, w^{k..} |=(b) f
////
LEMMA 5.2: Let c be a boolean expression, let R be an unclocked SERE,
and let w be a non-empty finite word over 2^P. If w |=(c) R,
then the last letter of w satisfies c.
PROOF: By induction over the structure of R. Let I = |w| - 1.
It must be shown that w^I |= c.
* R = b.
w |=(c) b
=> w^I |= c & b
=> w^I |= c
* R = {r}.
w |=(c) {r}
iff w |=(c) r
=> [induction]
w^I |= c
* R = r_1 ; r_2.
w |=(c) r_1 ; r_2
iff there exist x,y such that w = xy and x |=(c) r_1 and y |=(c) r_2
=> [induction]
there exist x,y such that w = xy and if x is non-empty then the
last letter of x satisfies c and if y is non-empty then the
last letter of y satisfies c
=> w^I |= c
* R = r_1 : r_2.
w |=(c) r_1 : r_2
iff there exist x,y,z such that w = xyz and |y| = 1 and
xy |=(c) r_1 and yz |=(c) r_2
=> [induction]
the last letter of yz satisfies c
=> w^I |= c
* R = {r_1} | {r_2}.
w |=(c) {r_1} | {r_2}
iff w |=(c) r_1 or w |=(c) r_2
=> [induction]
w^I |= c
* R = {r_1} && {r_2}.
w |=(c) {r_1} && {r_2}
iff w |=(c) r_1 and w |=(c) r_2
=> [induction]
w^I |= c
* R = r[*].
w |=(c) r[*]
iff [w is non-empty]
there exist w_1,...,w_j non-empty such that w = w_1...w_j
and for all i such that 1 <= i <= j, w_i |=(c) r
=> [induction]
the last letter of w_j satisfies c
=> w^I satisfies c
////
LEMMA 5.3: Let c be a boolean expression, let phi be an unclocked
SVA property fragment, and let w be an infinite word over 2^P such
that w^0 |= c. Then the following are equivalent:
1. w |=(TRUE) T(@(c) phi) .
2. w |=(TRUE) T(phi)@c .
PROOF:
* phi = R.
w |=(TRUE) T(@(c) R)
iff w |=(TRUE) {1} |-> {M(@(c) R)}!
iff [Lemma 4.1]
there exists j >= 0 such that w^{0,j} |=(TRUE) M(@(c) R)
iff there exists j >= 0 such that w^{0,j} |=(TRUE) {M(R)}@c
iff [w^0 |= c]
there exists j >= 0 such that w^{0,j} |=(c) M(R)
iff [since w^0 |= c, w^{0,i} |=(c) 1 iff i = 0]
w |=(c) {1} |-> {M(r)}!
iff w |=(c) T(R)
iff [w^0 |= c]
w |=(TRUE) T(R)@c
* phi = not b.
w |=(TRUE) T(@(c) not b)
iff w |=(TRUE) T(@(c) !b)
iff [proof for phi = R]
w |=(TRUE) T(!b)@c
iff [w^0 |= c]
w |=(c) T(!b)
iff w |=(c) {1} |-> {!b}
iff [w^0 |= c]
w^0 |= !b
iff [w is over 2^P]
not(w^0 |= b)
iff [w^0 |= c]
not(w |=(c) {1} |-> {b})
iff not(w |=(c) T(b))
iff w |=(c) !T(b)
iff w |=(c) T(not b)
iff [w^0 |= c]
w |=(c) T(not b)@c
* phi = not R, R not a boolean expression.
w |=(TRUE) T(@(c) not R)
iff w |=(TRUE) !T(@(c) R)
iff not(w |=(TRUE) T(@(c) R))
iff [proof for phi = R]
not(w |=(TRUE) T(R)@c)
iff [w^0 |= c]
not(w |=(c) T(R))
iff w |=(c) !T(R)
iff w |=(c) T(not R)
iff [w^0 |= c]
w |=(TRUE) T(not R)@c
* phi = (R_1 |-> R_2).
w |=(TRUE) T(@(c) (R_1 |-> R_2))
iff w |=(TRUE) T((@(c) R_1 |-> @(c) R_2))
iff w |=(TRUE) {M(@(c) R_1)} |-> {M(@(c) R_2)}!
iff w |=(TRUE) {{M(R_1)}@c} |-> {{M(R_2)}@c}!
iff for all i >= 0 such that w^{0,i} |=(TRUE) {M(R_1)}@c,
there exists j >= i such that w^{i,j} |=(TRUE) {M(R_2)}@c
iff [w^0 |= c]
for all i >= 0 such that w^{0,i} |=(c) M(R_1),
there exists j >= i such that w^{i,j} |=(TRUE) {M(R_2)}@c
iff [by Lemma 5.2, if w^{0,i} |=(c) M(R_1), then w^i |= c]
for all i >= 0 such that w^{0,i} |=(c) M(R_1),
there exists j >= i such that w^{i,j} |=(c) M(R_2)
iff w |=(c) {M(R_1)} |-> {M(R_2)}!
iff w |=(c) T((R_1 |-> R_2))
iff [w^0 |= c]
w |=(TRUE) T((R_1 |-> R_2))@c
* phi = not (R_1 |-> R_2).
w |=(TRUE) T(@(c) not (R_1 |-> R_2))
iff w |=(TRUE) !T(@(c) (R_1 |-> R_2))
iff not(w |=(TRUE) T(@(c) (R_1 |-> R_2)))
iff [proof for phi = (R_1 |-> R_2)]
not(w |=(TRUE) T((R_1 |-> R_2))@c)
iff [w^0 |= c]
not(w |=(c) T((R_1 |-> R_2)))
iff w |=(c) !T((R_1 |-> R_2))
iff w |=(c) T(not(R_1 |-> R_2))
iff [w^0 |= c]
w |=(TRUE) T(not(R_1 |-> R_2))@c
* phi = (R_1 |-> not b).
w |=(TRUE) T(@(c) (R_1 |-> not b))
iff w |=(TRUE) T((@(c) R_1 |-> @(c) !b))
iff [proof for phi = (R_1 |-> R_2)]
for all i >= 0 such that w^{0,i} |=(c) M(R_1),
there exists j >= i such that w^{i,j} |=(c) M(!b)
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1),
there exists j >= i such that w^{i,j} |=(c) !b
iff [by Lemma 5.2, if w^{0,i} |=(c) M(R_1), then w^i |= c]
for all i >= 0 such that w^{0,i} |=(c) M(R_1), w^i |= !b
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1), not(w^i |= b)
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1),
not(w^{i..} |=(c) {1} |-> {b}!)
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1),
not(w^{i..} |=(c) {1} |-> {b}!)
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1),
w^{i..} |=(c) !({1} |-> {b}!)
iff w |=(c) {M(R_1)}(!({1} |-> {b}!))
iff w |=(c) {M(R_1)}(!({1} |-> {M(b)}!))
iff w |=(c) T((R_1 |-> not b))
iff [w^0 |= c]
w |=(TRUE) T((R_1 |-> not b))@c
* phi = (R_1 |-> not R_2), R_2 not a boolean expression.
w |=(TRUE) T(@(c) (R_1 |-> not R_2))
iff w |=(TRUE) T((@(c) R_1 |-> not @(c) R_2))
iff w |=(TRUE) {M(@(c) R_1)}(!({1} |-> {M(@(c) R_2)}!))
iff w |=(TRUE) {M(R_1)@c}(!({1} |-> {M(R_2)@c}!))
iff for all i >= 0 such that w^{0,i} |=(TRUE) M(R_1)@c,
w^{i..} |=(TRUE) !({1} |-> {M(R_2)@c}!)
iff for all i >= 0 such that w^{0,i} |=(TRUE) M(R_1)@c,
not(w^{i..} |=(TRUE) {1} |-> {M(R_2)@c}!)
iff for all i >= 0 such that w^{0,i} |=(TRUE) M(R_1)@c,
not(there exists j >= i such that w^{i,j} |=(TRUE) M(R_2)@c)
iff [w^0 |= c; by Lemma 5.2, if w^{0,i} |=(c) M(R_1), then w^i |= c]
for all i >= 0 such that w^{0,i} |=(c) M(R_1)
not(there exists j >= i such that w^{i,j} |=(c) M(R_2))
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1)
not(w^{i..} |=(c) {1} |-> {M(R_2)}!)
iff for all i >= 0 such that w^{0,i} |=(c) M(R_1)
w^{i..} |=(c) !({1} |-> {M(R_2)}!)
iff w |=(c) {M(R_1)}(!({1} |-> {M(R_2)}!))
iff w |=(c) T((R_1 |-> not R_2))
iff [w^0 |= c]
w |=(TRUE) T((R_1 |-> not R_2))@c
* phi = not (R_1 |-> not R_2).
w |=(TRUE) T(@(c) not (R_1 |-> not R_2))
iff w |=(TRUE) !(T(@(c) (R_1 |-> not R_2)))
iff not(w |=(TRUE) T(@(c) (R_1 |-> not R_2)))
iff [proofs for phi = (R_1 |-> not R_2), R_2 boolean and not]
not(w |=(TRUE) T((R_1 |-> not R_2))@c)
iff [w^0 |= c]
not(w |=(c) T((R_1 |-> not R_2)))
iff w |=(c) !T((R_1 |-> not R_2))
iff w |=(c) T(not(R_1 |-> not R_2))
iff [w^0 |= c]
iff w |=(TRUE) T(not(R_1 |-> not R_2))@c
////
PROPOSITION 5.1: Let A be a SVA assertion (understood to
have enabling condition 1) that does not involve
"disable iff", and let w be an infinite word over 2^P.
Then the following are equivalent:
1. w |= A .
2. w |=(TRUE) T(A) .
PROOF:
* A = always assert property psi.
w |= always assert property psi
iff for all i >= 0, w^{i..} |= psi
iff [Proposition 4.1]
for all i >= 0, w^{i..} |=(TRUE) T(psi)
iff [Lemma 5.1]
w |=(TRUE) always T(psi)
iff w |=(TRUE) T(always assert property psi)
* A = always @(b) assert property phi.
w |= always @(b) assert property phi
iff for all i >= 0 such that w^i |= b, w^{i..} |= @(b) phi
iff [Proposition 4.1]
for all i >= 0 such that w^i |= b, w^{i..} |=(TRUE) T(@(b) phi)
iff [Lemma 5.3]
for all i >= 0 such that w^i |= b, w^{i..} |=(TRUE) T(phi)@b
iff for all i >= 0 such that w^i |= b, w^{i..} |=(b) T(phi)
iff [Lemma 5.1]
w |=(TRUE) (always T(phi))@b
iff w |=(TRUE) T(always @(b) assert property phi)
* A = initial assert property psi.
w |= initial assert property psi
iff w |= psi
iff [Proposition 4.1]
w |=(TRUE) T(psi)
iff w |=(TRUE) T(initial assert property psi)
* A = initial @(b) assert property phi.
w |= initial @(b) assert property phi
iff if there exists i >= 0 such that w^i |= b, then for the first
such i, w^{i..} |= @(b) phi
iff [Proposition 4.1]
if there exists i >= 0 such that w^i |= b, then for the first
such i, w^{i..} |=(TRUE) T(@(b) phi)
iff [Lemma 5.3]
if there exists i >= 0 such that w^i |= b, then for the first
such i, w^{i..} |=(TRUE) T(phi)@b
iff if there exists i >= 0 such that w^i |= b, then for the first
such i, w^{i..} |=(b) T(phi)
iff w |=(TRUE) (T(phi))@b
iff w |=(TRUE) T(initial @(b) assert property phi)
////
===========================================================================
This archive was generated by hypermail 2b28 : Wed Apr 30 2003 - 17:36:57 PDT