Subject: RE: [sv-ac] negated boolean proposal
From: Bassam Tabbara (bassam@novas.com)
Date: Tue Oct 28 2003 - 15:51:16 PST
Roy, I think the following:
>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.
Is a dramatic and rather confusing statement. They are basically the
same (assuming you do not mean an "always" in the PSL part). The
strong/weak issue is I guess what you mean to emphasize (John addressed
that just now), granted, but the liveness/safety variation is not there,
"initial" in SVA does the job.
Thx,
-Bassam.
-- Dr. Bassam Tabbara Technical Manager, R&D Novas Software, Inc.http://www.novas.com (408) 467-7893
> -----Original Message----- > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On > Behalf Of Armoni, Roy > Sent: Tuesday, October 28, 2003 8:24 AM > To: Cindy Eisner > Cc: sv-ac@eda.org > Subject: RE: [sv-ac] negated boolean proposal > > > 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> > > <!-- Converted from text/rtf format --> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > FACE=3D"Comic Sans MS">Hi John,</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > 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.</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > 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.</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > FACE=3D"Comic Sans MS">I wonder what is the committee's take on = > > this?</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > FACE=3D"Comic Sans MS">Thanks,</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000000" > SIZE=3D2 = > > FACE=3D"Comic Sans MS"> Roy</FONT></SPAN></P> <BR> > > <UL DIR=3DLTR> > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT FACE=3D"Comic Sans = > > MS"></FONT> <FONT SIZE=3D1 FACE=3D"Tahoma">-----Original = > > Message-----</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><B><FONT SIZE=3D1 = > > FACE=3D"Tahoma">From: </FONT></B> <FONT SIZE=3D1 = > > FACE=3D"Tahoma">owner-sv-ac@eda.org [</FONT></SPAN><A = > > HREF=3D"mailto:owner-sv-ac@eda.org"><SPAN LANG=3D"en-us"><U><FONT = > > COLOR=3D"#0000FF" SIZE=3D1 = > > > FACE=3D"Tahoma">mailto:owner-sv-ac@eda.org</FONT></U></SPAN></A><SPAN > = > > LANG=3D"en-us"><FONT SIZE=3D1 > FACE=3D"Tahoma">] </FONT><B> <FONT > = > > SIZE=3D1 FACE=3D"Tahoma">On Behalf Of</FONT></B> <FONT SIZE=3D1 = > > FACE=3D"Tahoma">John Havlicek</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><B><FONT SIZE=3D1 = > > FACE=3D"Tahoma">Sent: </FONT></B> <FONT SIZE=3D1 = > > FACE=3D"Tahoma">Tuesday, October 14, 2003 12:03 AM</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><B><FONT SIZE=3D1 = > > FACE=3D"Tahoma">To: </FONT></B> > <FONT SIZE=3D1 > = > > FACE=3D"Tahoma">sv-ac@eda.org</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><B><FONT SIZE=3D1 = > > > FACE=3D"Tahoma">Subject: &n > bsp;</FONT > = > > ></B> <FONT SIZE=3D1 FACE=3D"Tahoma">[sv-ac] negated boolean = > > proposal</FONT></SPAN></P> > > > > <P DIR=3DLTR><SPAN LANG=3D"en-us"><FONT COLOR=3D"#000080" > SIZE=3D2 = > > FACE=3D"Comic Sans MS"> << File: negbool_proposal.txt = > > >> </FONT></SPAN></P> </UL> > > </BODY> > > </HTML> > > ------_=_NextPart_001_01C393DE.42F7C49B-- > > > >
This archive was generated by hypermail 2b28 : Tue Oct 28 2003 - 15:51:56 PST