Re: [sv-ac] negated boolean proposal

Subject: Re: [sv-ac] negated boolean proposal
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Oct 28 2003 - 12:18:29 PST

Next message: Bassam Tabbara: "RE: [sv-ac] FW: LRM corrections"
Previous message: David W. Smith: "RE: [sv-ac] Property definition in $root"
In reply to: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Next in thread: Bassam Tabbara: "RE: [sv-ac] negated boolean proposal"
Next in thread: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Reply: John Havlicek: "Re: [sv-ac] negated boolean proposal"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Hi Roy:

As you know, there has been a lot of work in the SVA/PSL Alignment Subcommittee
to define a mapping from a subset of SVA to PSL and to prove semantic
correspondence under the mapping.

In the proposed PSL 1.1, strong booleans are ornamented with a trailing "!",
while in SVA 3.1, the naked boolean is strong. This is not syntactically
aligned, but it is (fairly well) semantically aligned. The mapping accounts
for the syntactic difference at the property level by defining

   T(@(c) b) = {M(@(c)b)}!
             = {M(b)@c}!
             = {b@c}!

The weak boolean can be expressed in SVA 3.1 using a device, such as
not(!b or !b).

Best regards,

John H.

>
> 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:       </FONT
> =
> > > [sv-ac] negated boolean =
> > proposal
> >
> > > FACE=3D"Comic Sans MS"> << File: negbool_proposal.txt =
> > >> 
> > </UL>
> > </BODY>
> > </HTML>
> > ------_=_NextPart_001_01C393DE.42F7C49B--
>
>
>

Next message: Bassam Tabbara: "RE: [sv-ac] FW: LRM corrections"
Previous message: David W. Smith: "RE: [sv-ac] Property definition in $root"
In reply to: Armoni, Roy: "RE: [sv-ac] negated boolean proposal"
Next in thread: Bassam Tabbara: "RE: [sv-ac] negated boolean proposal"
Next in thread: 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 : Tue Oct 28 2003 - 12:19:16 PST