Subject: RE: [sv-ac] SVA/PSL equivalences
From: Erich Marschner (erichm@cadence.com)
Date: Thu Nov 06 2003 - 13:05:03 PST
John,
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?
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Cell: +1 410 294 2599 Email: erichm@comcast.net
| -----Original Message-----
| From: Armoni, Roy [mailto:roy.armoni@intel.com]
| Sent: Thursday, November 06, 2003 2:51 PM
| To: john.havlicek@motorola.com
| Cc: eisner@il.ibm.com; dana@wisdom.weizmann.ac.il; sv-ac@eda.org
| Subject: RE: [sv-ac] SVA/PSL equivalences
|
|
| Hi John,
|
| The discussion we had on this thread made me think more about the SVA
| semantics, and actually, I'm a little worried now. I think
| that before
| we take care of synch and equivalence between SVA and PSL, we need to
| first make sure that each language is consistent (by
| consistent here, I
| mean in the normal English sense, rather than the
| mathematical sense).
|
| One important check that I think SVA has to pass, is that
| whenever both
| of "||" and "or" may be applied, they will have the same semantics.
| Similarly for "and" pair and the "not" pair. The issue that this
| discussion raises is that although when considered
| separately, "||" and
| "or" are equivalent, then in some contexts they produce different
| results, that is:
| initial assert @(c) not (x || y)
| is different than
| initial assert @(c) not (x or y)
|
| Similarly, the following pair is different:
| always assert @(c) not (x || y) // livness
| always assert @(c) not (x or y) // safety
|
| This is a point that I missed in the past, but now that I am aware of
| it, I think that we should fix.
| What do you think?
|
| Regards,
| Roy
|
|
| -----Original Message-----
| From: John Havlicek [mailto:john.havlicek@motorola.com]
| Sent: Thursday, October 30, 2003 5:42 PM
| To: Armoni, Roy
| Cc: john.havlicek@motorola.com; eisner@il.ibm.com;
| dana@wisdom.weizmann.ac.il; sv-ac@eda.org
| Subject: Re: [sv-ac] SVA/PSL equivalences
|
|
| Hi Roy:
|
| I agree with you on this pair. Of course, my proposed change
| to the SVA semantics will fix this problem and make these two
| equivalent.
|
| Best regards,
|
| John H.
|
| >
| > Hi John,
| >
| > You are right. The ones that are not equivalent are:
| > initial assert @(c) not (x || y)
| > and
| > (!(x! | y!)) @c
| >
| > The SVA version is a liveness property while the PSL is a safety.
| >
| > Regards,
| > Roy
| >
| >
|
This archive was generated by hypermail 2b28 : Thu Nov 06 2003 - 13:05:41 PST