RE: [sv-ac] negated boolean proposal

Subject: RE: [sv-ac] negated boolean proposal
From: Armoni, Roy (roy.armoni@intel.com)
Date: Tue Oct 28 2003 - 08:24:07 PST

Next message: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Previous message: Steve Grout: "[sv-ac] test - please ignore"
Maybe in reply to: John Havlicek: "[sv-ac] negated boolean proposal"
Next in thread: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Next in thread: Armoni, Roy: "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"
Reply: Bassam Tabbara: "RE: [sv-ac] negated boolean proposal"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Hi Cindy,

The reason I wrote that the proposed change will not create a disruption
to the alignment effort is because SVA and PSL are not fully aligned.
Take for instance the SVA formula
initial assert @(c) b
which is a liveness property in SVA, while a straightforward rewrite to
PSL results in
b@c
which is a safety property. I believe that a similar effect is created
when "initial" is replaced by "always".

In general, I wouldn't underestimate the effect of liveness properties
that are created without the user intention.

Regards,
Roy

-----Original Message-----
From: Cindy Eisner [mailto:EISNER@il.ibm.com]
Sent: Tuesday, October 21, 2003 11:03 AM
To: Armoni, Roy
Cc: john.havlicek@motorola.com; sv-ac@eda.org; Dana Fisman;
dana@wisdom.weizmann.ac.il
Subject: RE: [sv-ac] negated boolean proposal

roy,

i disagree that what you have in mind does not cause disruption to the
alignment efforts. changing to immediate booleans is a huge disruption,
as
it is completely opposite to the approach taken in psl.

i would not worry too much about generations of engineers pondering the
strength of boolean expressions. first, i have never known one to worry
about it yet. second, the issue is relevant only on infinite paths
where
the clock never ticks. so i don't see much potential for future worry
from
the user community either.

regards,

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

"Armoni, Roy" <roy.armoni@intel.com>@eda.org on 10/16/2003 05:36:56 PM

Sent by: owner-sv-ac@eda.org

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: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Previous message: Steve Grout: "[sv-ac] test - please ignore"
Maybe in reply to: John Havlicek: "[sv-ac] negated boolean proposal"
Next in thread: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Next in thread: Armoni, Roy: "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"
Reply: Bassam Tabbara: "RE: [sv-ac] negated boolean proposal"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

This archive was generated by hypermail 2b28 : Tue Oct 28 2003 - 08:25:03 PST