Subject: RE: [sv-ac] SVA/PSL equivalences
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Nov 06 2003 - 11:50:38 PST
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 - 11:51:21 PST