Subject: RE: [sv-ac] SVA/PSL equivalences
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Nov 10 2003 - 09:56:43 PST
Hi John,
Please refer to my previous note on this thread as a "raising concerns"
note. It's not that I had some specific solution in mind, but I am
worried now about the internal lack of equivalence between "||" and "or"
in SVA semantics.
Let me try to formulate what I think should be a sanity check for SVA
semantics:
Let P be an SVA property, let B be a Boolean expression sub property of
P such that for every sub property Q of P, if B is a sub property of Q,
then Q is not a Boolean expression.
(1) If B is "X || Y", then denote by P_B_or the property P in which B is
replaced by "X or Y", and require that P is equivalent to P_B_or.
(2) If B is "X && Y", then denote by P_B_and the property P in which B
is replaced by "X and Y", and require that P is equivalent to P_B_and.
(3) If B is "!X", then denote by P_B_not the property P in which B is
replaced by "not X", and require that P is equivalent to P_B_not.
What do you think?
Regards,
Roy
-----Original Message-----
From: John Havlicek [mailto:john.havlicek@motorola.com]
Sent: Thursday, November 06, 2003 11:00 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 that SVA 3.1 semantics needs to be fixed. I sent a proposal
for doing this by changing the clock rewrite rules for "@(c) not b"
and "@(c) not R".
Under my proposal,
initial assert @(c) not (x || y)
and
initial assert @(c) not (x or y)
are equivalent, as are
always assert @(c) not (x || y)
and
always assert @(c) not (x or y)
Under my proposal,
initial assert @(c) !b
and
initial assert @(c) not b
are not equivalent, although
initial @(c) assert !b
and
initial @(c) assert not b
are equivalent for proper words.
If you don't like this solution, why don't you write down a complete
alternative proposal and submit it to the committee for discussion?
I am also happy to discuss this off the reflector, but I still need
for you to write down your criteria and your proposal so I know
what you are trying to do.
Best regards,
John H.
>
> 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]=20
> 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=20
> to the SVA semantics will fix this problem and make these two=20
> equivalent.
>
> Best regards,
>
> John H.
>
> >=20
> > Hi John,
> >=20
> > You are right. The ones that are not equivalent are:
> > initial assert @(c) not (x || y)
> > and
> > (!(x! | y!)) @c
> >=20
> > The SVA version is a liveness property while the PSL is a safety.
> >=20
> > Regards,
> > Roy
> >=20
> >=20
This archive was generated by hypermail 2b28 : Mon Nov 10 2003 - 09:57:25 PST