RE: [sv-ac] negated boolean proposal

Subject: RE: [sv-ac] negated boolean proposal
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Oct 16 2003 - 09:09:46 PDT

Next message: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Previous message: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Maybe in reply to: John Havlicek: "[sv-ac] negated boolean proposal"
Next in thread: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Maybe reply: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Reply: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

... and I forgot to mention that the rewrite rule for clocked Booleans
should be simplified to:
@(c) b --> b

-----Original Message-----
From: Armoni, Roy
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]
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?
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
between SVA and PSL semantics?

* How significant is the change in practice?

Best regards,

John H.

>
> Hi John,
>
> 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.
>
> 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.
>
> I wonder what is the committee's take on this?
>
> Thanks,
>
> Roy
>
>
> -----Original Message-----
>
> From: owner-sv-ac@eda.org [ <mailto:owner-sv-ac@eda.org>
> mailto:owner-sv-ac@eda.org] On Behalf Of John Havlicek
>
> Sent: Tuesday, October 14, 2003 12:03 AM
>
> To: sv-ac@eda.org
>
> Subject: [sv-ac] negated boolean proposal
>
> << File: negbool_proposal.txt >>=20
>
>
> ------_=_NextPart_001_01C393DE.42F7C49B
> Content-Type: text/html;
> charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
>
> <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
> <HTML>
> <HEAD>
>
> <META NAME=3D"Generator" CONTENT=3D"MS Exchange Server version =
> 6.0.6487.1">
> <TITLE>RE: [sv-ac] negated boolean proposal</TITLE>
> </HEAD>
> <BODY>
> 
>
> FACE=3D"Comic Sans MS">Hi John,
>
> FACE=3D"Comic Sans MS">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.
>
> FACE=3D"Comic Sans MS">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.
>
> FACE=3D"Comic Sans MS">I wonder what is the committee's take on =
> this?
>
> FACE=3D"Comic Sans MS">Thanks,
>
> FACE=3D"Comic Sans MS"> Roy
> 
> <UL DIR=3DLTR>
> MS"> -----Original =
> Message-----
>
> FACE=3D"Tahoma">From:   FACE=3D"Tahoma">owner-sv-ac@eda.org [<A =
> HREF=3D"mailto:owner-sv-ac@eda.org"> COLOR=3D"#0000FF" SIZE=3D1 =
> FACE=3D"Tahoma">mailto:owner-sv-ac@eda.org</A><SPAN
=
> LANG=3D"en-us">]  <FONT
=
> SIZE=3D1 FACE=3D"Tahoma">On Behalf Of FACE=3D"Tahoma">John Havlicek
>
> FACE=3D"Tahoma">Sent:   FACE=3D"Tahoma">Tuesday, October 14, 2003 12:03 AM
>
> FACE=3D"Tahoma">To:     FACE=3D"Tahoma">sv-ac@eda.org
>
> 
FACE=3D"Tahoma">Subject:        > [sv-ac] negated boolean =
> proposal
>
> FACE=3D"Comic Sans MS"> << File: negbool_proposal.txt =
> >> 
> </UL>
> </BODY>
> </HTML>
> ------_=_NextPart_001_01C393DE.42F7C49B--

Next message: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Previous message: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Maybe in reply to: John Havlicek: "[sv-ac] negated boolean proposal"
Next in thread: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Maybe reply: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Reply: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

This archive was generated by hypermail 2b28 : Thu Oct 16 2003 - 09:10:25 PDT