Subject: Re: [sv-ac] negated boolean proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Oct 17 2003 - 09:29:04 PDT
Roy:
I don't think the change is quite this simple. The way the
formal semantics handles something like
@(c1) b1 |=> @(c2) b2
will be drastically changed. How will the current semantics
of this property be achieved under your proposal?
Best regards,
John H.
>
> ... and I forgot to mention that the rewrite rule for clocked Booleans
> should be simplified to:
> @(c) b --> b
>
> -----Original Message-----
> From: Armoni, Roy=20
> 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
>
>
> Hi John,
>
> * Yes, what I have in mind requires changing to immediate Booleans.
>
> * 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) )
>
> * No, it will not cause any disruption whatsoever to the current state
> of the alignment between SVA and PSL.
>
> * 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.
>
> Regards,
> Roy
>
>
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@motorola.com]=20
> 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
>
>
> Roy:
>
> Can you be more specific about what you have in mind?=20
> I have the following questions about it.
>
> * Does it require changing to immediate booleans?
>
> * Does it require rewriting the entire SVA formal semantics?
>
> * Will it cause significant disruption of the current alignment=20
> between SVA and PSL semantics?
>
> * How significant is the change in practice?
>
> Best regards,
>
> John H.
>
> >=20
> > Hi John,
> >=20
> > 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. =
> At
> > the same time, I believe that 1. and 2. should have exactly the same
> > meaning - the difference between "!" and "not" is only syntactic.
> >=20
> > 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.
> >=20
> > I wonder what is the committee's take on this?
> >=20
> > Thanks,
> >=20
> > Roy
> >=20
> >=20
This archive was generated by hypermail 2b28 : Fri Oct 17 2003 - 09:29:58 PDT