Subject: Re: [sv-ac] negated boolean proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Oct 28 2003 - 10:29:45 PST
Roy:
I understand that both suggestions change the formal semantics.
I think that performing only the changes you wrote down
results in a much greater change to the semantics than what
I proposed.
Do you agree that
(*) @(c1) b1 |=> @(c2) b2
does not have the same semantics under your proposal as it
does in SVA 3.1? If not, can you sketch the argument for
why the semantics are the same. If so, my question remains,
how do I write a property whose semantics under your proposal
is the same as the semantics of (*) in SVA 3.1?
Best regards,
John H.
> content-class: urn:content-classes:message
> X-MimeOLE: Produced By Microsoft Exchange V6.0.6487.1
> Date: Tue, 28 Oct 2003 18:24:05 +0200
> X-MS-Has-Attach:
> X-MS-TNEF-Correlator:
> Thread-Topic: [sv-ac] negated boolean proposal
> Thread-Index: AcOUy+hX5xOP3VdOSHO/9lO448zgLQITMlqQ
> From: "Armoni, Roy"<roy.armoni@intel.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 28 Oct 2003 16:24:05.0523 (UTC) FILETIME=[E7F80E30:01C39D6F]
>
> Hi John,
>
> I hope that it is understood that both your original proposal, and the
> extension that I propose are not merely a different way to write the
> same semantics, but a slight change to the formal semantics.
>
> Regards,
> Roy
>
>
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@motorola.com]=20
> Sent: Friday, October 17, 2003 6:29 PM
> To: Armoni, Roy
> Cc: john.havlicek@motorola.com; sv-ac@eda.org
> Subject: Re: [sv-ac] negated boolean proposal
>
>
> Roy:
>
> I don't think the change is quite this simple. The way the=20
> formal semantics handles something like
>
> @(c1) b1 |=3D> @(c2) b2
>
> will be drastically changed. How will the current semantics
> of this property be achieved under your proposal?
>
> Best regards,
>
> John H.
>
>
> >=20
> > ... and I forgot to mention that the rewrite rule for clocked =
> Booleans
> > should be simplified to:
> > @(c) b --> b
> >=20
> > -----Original Message-----
> > From: Armoni, Roy=3D20
> > Sent: Thursday, October 16, 2003 5:36 PM
> > To: 'john.havlicek@motorola.com'
> > Cc: sv-ac@eda.org
> > Subject: RE: [sv-ac] negated boolean proposal
> >=20
> >=20
> > Hi John,
> >=20
> > * Yes, what I have in mind requires changing to immediate Booleans.
> >=20
> > * No, it does not require rewriting the entire SVA formal semantics.
> > Actually, after reviewing again the way SVA semantics is written, =
> then
> > in addition to your proposal, it requires only one line change, that
> is
> > the rewrite rule of ##1 has to be changed to:
> > @(c) (R1 ##1 R2) --> ( (@(c) R1) ##1 !c[*0:$] ##1 c ##0 (@(c) R2) )
> >=20
> > * No, it will not cause any disruption whatsoever to the current =
> state
> > of the alignment between SVA and PSL.
> >=20
> > * The significant of this change is for generations of engineers for
> > whom we will save the bother of figuring out the strength of a
> property
> > and its strength under negation.
> >=20
> > Regards,
> > Roy
> >=20
> >=20
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@motorola.com]=3D20
> > Sent: Thursday, October 16, 2003 4:08 PM
> > To: Armoni, Roy
> > Cc: john.havlicek@motorola.com; sv-ac@eda.org
> > Subject: Re: [sv-ac] negated boolean proposal
> >=20
> >=20
> > Roy:
> >=20
> > Can you be more specific about what you have in mind?=3D20
> > I have the following questions about it.
> >=20
> > * Does it require changing to immediate booleans?
> >=20
> > * Does it require rewriting the entire SVA formal semantics?
> >=20
> > * Will it cause significant disruption of the current alignment=3D20
> > between SVA and PSL semantics?
> >=20
> > * How significant is the change in practice?
> >=20
> > Best regards,
> >=20
> > John H.
> >=20
> > >=3D20
> > > Hi John,
> > >=3D20
> > > Thanks for raising this issue. The difference in the semantics
> > between
> > > 1. on one hand and 3.,4.,5. on the other hand is indeed bothering.
> =3D
> > At
> > > the same time, I believe that 1. and 2. should have exactly the =
> same
> > > meaning - the difference between "!" and "not" is only syntactic.
> > >=3D20
> > > I believe that there is no real dilemma here and we can make all of
> > > 1.-5. equivalent, but it requires some work, much more than the
> small
> > > change in your proposal. However, I am willing to invest this work
> > for
> > > the benefit of all the future SVAs that are going to be written out
> > > there.
> > >=3D20
> > > I wonder what is the committee's take on this?
> > >=3D20
> > > Thanks,
> > >=3D20
> > > Roy
> > >=3D20
> > >=3D20
This archive was generated by hypermail 2b28 : Tue Oct 28 2003 - 10:30:34 PST