Subject: Re: [sv-ac] SVA/PSL equivalences
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Nov 06 2003 - 13:47:40 PST
Hi Erich:
> Isn't this question related to the 'quality metrics' we discussed for =
> PSL quite a while ago - perhaps a year ago now? I seem to recall that =
> we identified the same problem - essentially, whether standard boolean =
> logic axioms applied as usual to conjunction/disjunction of temporal =
> properties ... Am I correct? If so, I seem to recall that, as the =
> semantics evolved, you were eventually able to show that expected =
> equivalences did in fact hold. Do those analyses need to be redone, or =
> are they still valid for PSL 1.1? Or are my recollections from last =
> year just totally confused?
Yes, it is related, but we never had the "consistency" between
boolean- and property-level operators on our list. This is because
the PSL semantics hides most of the boolean layer.
Notice too that my proposal for changing the clock rewrite rule for
negated boolean in SVA 3.1 (the one we approved in the alignment
subcommittee) achieves "consistency" for conjunction and disjunction.
It is only negation that has an "inconsistency", and this only
when it is used in the assertion forms that apply the clock within
the "assert" instead of without.
The question is, what do we want to give up to make formula negation
of booleans equivalent to boolean negation in all cases where both
are allowed? Strenghless clock and go back to strong and weak clocks,
even though we have no notation for them in SVA? Aligned booleans and
give up the projection view in the singly-clocked case? Something else?
In any case, my intuition is that "fixing" the "inconsistency" of
negation will require overhauling the semantics. I will be happy
to review any complete proposal to do this. However, I think that
if we make such a semantic change in one of SVA/PSL, then we need
to make it in the other.
It would be great to review the old criteria. We have to be
prepared to revise them, though, since they were not written
for the \top,\bot and strong/weak boolean approach to the
semantics. I also don't think we ever satisfied them all
in full generality. I've attached the latest list (from 13 Nov 2002)
below.
Best regards,
John H.
=========================
PRELIMINARIES
NOTATION: Below,
i. f,g,f',g' denote FL properties.
ii. r,s,t denote SEREs.
iii. b,c denote boolean expressions.
////
DEFINITION 1: If f,g are unclocked FL properties, then
"f is unclocked equivalent to g" means for all pi, for all i
pi,i |= f iff pi,i |= g.
////
REMARK: An unclocked FL property cannot have instances of "@",
"rose", "fell", "posedge", etc.
////
DEFINITION 2: If f,g are FL properties, then "f is equivalent to g" means
for all pi, for all clock contexts K, and for all i such that pi,i |= K,
pi,i |=(K) f iff pi,i |=(K) g
////
REMARK: Note that "f is equivalent to g" is a clocked equivalence. Most
equivalences in the requirements below are clocked equivalences, so this
convention is in the interest of brevity.
////
REQUIREMENTS
1. If there is a schema "for any unclocked FL formulas f1,...,fn:
F(f1,...,fn) is unclocked equivalent to G(f1,...,fn)", then there is
also a schema "for any clocked FL formulas f1,...,fn: F(f1,...,fn) is
equivalent to G(f1,...,fn)".
2. If g is a subproperty of f, if f' results from f by substituting
g' for g, and if g' is equivalent to g, then f' is equivalent to f.
3. Let f be an unclocked FL formula. Let I = {i : w^i |= c}. Let
w|_c be the word obtained from w by first restricting its domain
to I and then reindexing. If I is not empty, then the following are
equivalent statements:
1. w |=(T) f @ c.
2. w |=(T) f @ c!.
3. w|_c |= f.
4. 1. If pi,i |=(c!) f, then there exists j >= i such that pi,j |= c.
2. If there does not exist j >= i such that pi,j |= c, then pi,j |=(c) f.
5. 1. If pi,i |=(c!) f, then pi,i |=(c) f.
2. If pi,i |=(c) f and if there exist infinitely many j >= i such that
pi,j |= c, then pi,i |=(c!) f.
6. 1. !!f is equivalent to f.
2. f && f is equivalent to f.
3. f && g is equivalent to g && f.
4. TRUE && f is equivalent to f.
5. FALSE && f is equivalent to FALSE.
6. f || g is equivalent to !(!f && !g).
7. For any context K, pi,i |=(K) f && g iff both pi,i |=(K) f and pi,i |=(K) g.
8. 1. "f until! g" is equivalent to "!(!g until_ !f)".
2. "f until!_ g" is equivalent to "!(!g until !f)".
3. "f until g" is equivalent to "!(!g until!_ !f)".
4. "f until_ g" is equivalent to "!(!g until! !f)".
9. For any context K, if pi,i |=(K) {r} |-> {s}!, then pi,i |=(K) {r} |-> {s}.
10. "f until! g" is equivalent to "g || (f && next! f until! g)".
11. "eventually! f" is equivalent to "f || next! eventually! f".
12. "always f" is equivalent to "f && next always f".
13. 1. "{TRUE}(f)" is equivalent to f.
2. "{FALSE}(f)" is equivalent to TRUE.
3. "{TRUE[*]}(f)" is equivalent to "always f".
4. "{FALSE} |-> {r}!" is equivalent to TRUE.
5. "{FALSE} |-> {r}" is equivalent to TRUE.
6. "{TRUE} |-> {TRUE[*];b}!" is equivalent to "eventually! b"
7. "{TRUE} |-> {TRUE[*];r}!" is equivalent to "eventually! ({TRUE} |-> {r}!)"
14. 1. "{r}(f && g)" is equivalent to "{r}(f) && {r}(g)".
2. "{r}({s}(f))" is equivalent to "{r:s}(f)".
3. "{r}({s} |-> {t}!)" is equivalent to "{r:s} |-> {t}!".
4. "{r}({s} |-> {t})" is equivalent to "{r:s} |-> {t}".
This archive was generated by hypermail 2b28 : Fri Nov 07 2003 - 01:19:17 PST