Subject: Re: [sv-ac] SVA/PSL equivalences
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Nov 06 2003 - 12:59:52 PST
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 : Thu Nov 06 2003 - 13:00:35 PST