Accellera SuperVerilog Assertion Activity: Re: [sv-ac] FW: [sv-e

From: Surrendra Dudani <Surrendra.Dudani@synopsys.com>
Date: Tue Apr 13 2004 - 07:34:47 PDT

I agree with John. Since we have generalized "not" as a property level
operator, it is not a good idea to restrict language forms. I believe
restrictions should only be placed on generalized operators when there are
complexities of implementation, or semantic difficulties (or sometimes, we
run out of time to improve the language). There are many non-intuitive
property forms from usage point of view, just like many non-intuitive
programs. I think linting or other debugging aids, customized for
particular applications/users, are far more useful in such cases.
Surrendra
At 10:46 PM 4/12/2004 -0500, you wrote:
>All:
>
>I do not think these forms should be illegal in SVA.
>They are not illegal in PSL. "not" in SVA correponds
>to negation in PSL, not to "never".
>
>Best regards,
>
>John H.
>
>
> > X-Authentication-Warning: server.eda.org: majordom set sender to
> owner-sv-ac@eda.org using -f
> > From: "David W. Smith" <dwsmith@synopsys.com>
> > Date: Mon, 12 Apr 2004 11:52:23 -0700
> > X-Priority: 3 (Normal)
> > X-MSMail-Priority: Normal
> > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
> > Importance: Normal
> > Sender: owner-sv-ac@eda.org
> > Precedence: bulk
> > X-Scan-Signature: 9d151aeb10af3ddbe92f5aedd916f4e6
> >
> > This is a multi-part message in MIME format.
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0
> > Content-Type: multipart/alternative;
> > boundary="----=_NextPart_001_003B_01C42084.9E3CE7A0"
> >
> > ------=_NextPart_001_003B_01C42084.9E3CE7A0
> > Content-Type: text/plain;
> > charset="us-ascii"
> > Content-Transfer-Encoding: 7bit
> >
> > The attached messages came to the SV-EC reflector but are more
> > appropriate for the SV-AC committee.
> >
> >
> >
> > Regards
> >
> > David
> >
> >
> >
> > -----Original Message-----
> > From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of
> > VhdlCohen@aol.com
> > Sent: Friday, April 09, 2004 3:04 PM
> > To: David.Smith@Synopsys.COM; sv-ec@eda.org
> > Cc: sri@noveldv.com
> > Subject: [sv-ec] not (a |->b), not(a |=> b) disallowed?
> >
> >
> >
> > The following property expressions should be disallowed in the LRM:
> >
> > not (a |->b), // by "a" or "b" I mean the sequences "a" "b"
> >
> > not(a |=> b)
> >
> > Rationale: from FROM LRM: 17.11.1 Implication
> > "If there is no match of the antecedent sequence_expr from a given
> > start point, then evaluation of the implication
> > from that start point succeeds vacuously and returns true"
> >
> > Thus, is "a" is false, (a |-> b) or (a |=>b) become TRUE, and "not(a
> > |-> b)" or "not(a |=>b)" becomes FALSE, or failure.
> >
> > That is not the intent here.
> >
> > In PSL, we disallow a "never {a} |-> {b}" or "never {a} |=> {b}"
> >
> >
> >
> > By the way, one could express the never implication with sequences as:
> >
> > (a |-> b |-> 'false)
> >
> > Ben
> >
> >
> > ------------------------------------------------------------------------
> > -----
> > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
> > http://www. <http://www.vhdlcohen.com/> vhdlcohen.com/ vhdlcohen@aol.com
> >
> > Author of following textbooks:
> > * Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004
> > isbn 0-9705394-6-0
> > * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> > 0-9705394-2-8
> > * Component Design by Example ", 2001 isbn 0-9705394-0-1
> > * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
> > 0-7923-8474-1
> > * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn
> > 0-7923-8115
> > ------------------------------------------------------------------------
> > ------
> >
> >
> > ------=_NextPart_001_003B_01C42084.9E3CE7A0
> > Content-Type: text/html;
> > charset="us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
> > <html>
> > <head>
> >
> > <meta name=3DGenerator content=3D"Microsoft Word 10 (filtered)">
> > <style>
> > 
> > </style>
> > </head>
> > <body lang=3DEN-US link=3Dblue vlink=3Dblue id=3D"role_body" =
> > bottomMargin=3D7
> > leftmargin=3D7 topmargin=3D7 rightMargin=3D7>
> > <div class=3DSection1>
> > <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial =
> > id=3D"role_document"><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:navy'>The attached =
> > messages
> > came to the SV-EC reflector but are more appropriate for the SV-AC =
> > committee.</span></font></p>
> > <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:navy'> </span></font></p>
> > <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:navy'>Regards</span></font></p>
> > <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:navy'>David</span></font></p>
> > <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3D"Times New =
> > Roman"><span
> > style=3D'font-size:10.0pt;color:navy'> </span></font></p>
> > <p class=3DMsoNormal><font size=3D2 face=3DTahoma><span =
> > style=3D'font-size:10.0pt;
> > font-family:Tahoma'>-----Original Message-----<br>
> > <b><span style=3D'font-weight:bold'>From:</span></b> =
> > owner-sv-ec@eda.org
> > [mailto:owner-sv-ec@eda.org] <b><span style=3D'font-weight:bold'>On =
> > Behalf Of </span></b>VhdlCohen@aol.com<br>
> > <b><span style=3D'font-weight:bold'>Sent:</span></b> =
> > </span></font><font size=3D2 face=3DTahoma><span =
> > style=3D'font-size:10.0pt;font-family:Tahoma'>Friday, April
> > 09, 2004</span></font><font size=3D2 face=3DTahoma><span =
> > style=3D'font-size:10.0pt;
> > font-family:Tahoma'> </span></font><font size=3D2 face=3DTahoma><span
> > style=3D'font-size:10.0pt;font-family:Tahoma'>3:04 =
> > PM</span></font><font size=3D2
> > face=3DTahoma><span style=3D'font-size:10.0pt;font-family:Tahoma'><br>
> > <b><span style=3D'font-weight:bold'>To:</span></b> =
> > David.Smith@Synopsys.COM;
> > sv-ec@eda.org<br>
> > <b><span style=3D'font-weight:bold'>Cc:</span></b> sri@noveldv.com<br>
> > <b><span style=3D'font-weight:bold'>Subject:</span></b> [sv-ec] not (a =
> > |->b), not(a
> > |=3D> b) disallowed? </span></font></p>
> > <p class=3DMsoNormal><font size=3D3 face=3D"Times New Roman"><span =
> > style=3D'font-size:
> > 12.0pt'> </span></font></p>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>The following property =
> > expressions should
> > be disallowed in the LRM: </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><strong><b><font size=3D2 color=3Dblack =
> > face=3DArial><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:black'>not (a =
> > |->b),</span></font></b></strong><font
> > size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;
> > color:black'>   // by "a" or "b" I
> > mean the sequences "a" "b"</span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><strong><b><font size=3D2 color=3Dblack =
> > face=3DArial><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:black'>not(a |=3D> =
> > b)</span></font></b></strong><font
> > size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;
> > color:black'>  </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>Rationale:   from FROM =
> > LRM:
> > 17.11.1 Implication<br>
> > </span></font><strong><b><font size=3D2 color=3Dred face=3DArial><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:red'>  "If =
> > there is
> > no match</span></font></b></strong><strong><b><font size=3D2 =
> > color=3Dblack
> > face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;color:black'> =
> > </span></font></b></strong><strong><b><font
> > size=3D2 color=3Dred face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;
> > color:red'>of the antecedent =
> > sequence</span></font></b></strong><strong><b><font
> > size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;
> > color:black'>_</span></font></b></strong><font size=3D2 color=3Dblack =
> > face=3DArial><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:black'>expr from a =
> > given start
> > point, then evaluation of the implication<br>
> > from that start point succeeds vacuously </span></font><strong><b><font =
> > size=3D2
> > color=3Dred face=3DArial><span =
> > style=3D'font-size:10.0pt;font-family:Arial;
> > color:red'>and returns true" </span></font></b></strong></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>Thus, is "a" is =
> > false,  <strong><b><font
> > face=3DArial><span style=3D'font-family:Arial'>(a |-> =
> > b)</span></font></b></strong>
> > or <strong><b><font face=3DArial><span style=3D'font-family:Arial'>(a =
> > |=3D>b)</span></font></b></strong>
> > become TRUE, and "<strong><b><font face=3DArial><span =
> > style=3D'font-family:
> > Arial'>not(a |-> b</span></font></b></strong>)" or =
> > <strong><b><font
> > face=3DArial><span style=3D'font-family:Arial'>"not(a =
> > |=3D>b)"</span></font></b></strong>
> >  becomes FALSE, or failure. </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>That is not the intent =
> > here.  </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>In PSL, we disallow a =
> > <strong><b><font
> > face=3DArial><span style=3D'font-family:Arial'>"never {a} |-> =
> > {b}" </span></font></b></strong>or<strong><b><font
> > face=3DArial><span style=3D'font-family:Arial'> "never {a} =
> > |=3D> {b}"</span></font></b></strong></span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'> </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'>By the way, one could express the =
> > never
> > implication with sequences as: </span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'> (a |-> b |-> =
> > 'false)</span></font></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><strong><b><font size=3D2 color=3Dblack =
> > face=3DArial><span
> > style=3D'font-size:10.0pt;font-family:Arial;color:black'>Ben</span></fon=
> > t></b></strong></p>
> > </div>
> > <div>
> > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3DArial><span =
> > style=3D'font-size:
> > 10.0pt;font-family:Arial;color:black'> </span></font><font =
> > size=3D1
> > color=3Dblack face=3DArial FAMILY=3DSANSSERIF PTSIZE=3D8><span =
> > style=3D'font-size:7.5pt;
> > font-family:Arial;color:black'>-----------------------------------------=
> > ------------------------------------<br>
> > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 <br>
> > <a href=3D"http://www.vhdlcohen.com/">http://www.<b><span =
> > style=3D'font-weight:
> > bold'>vhdlcohen</span></b>.com/</a> vhdlcohen@aol.com <br>
> > Author of following textbooks: <br>
> > * <b><span style=3D'font-weight:bold'>Using PSL/SUGAR for Formal and =
> > Dynamic
> > Verification 2nd Edition, </span></b>2004 isbn 0-9705394-6-0<br>
> > * <b><span style=3D'font-weight:bold'>Real Chip Design and Verification =
> > Using
> > Verilog and VHDL</span></b>, 2002 isbn 0-9705394-2-8 <br>
> > * <b><span style=3D'font-weight:bold'>Component Design by =
> > Example</span></b>
> > ", 2001 isbn 0-9705394-0-1<br>
> > * <b><span style=3D'font-weight:bold'>VHDL Coding Styles and =
> > Methodologies, 2nd
> > Edition</span></b>, 1999 isbn 0-7923-8474-1<br>
> > * <b><span style=3D'font-weight:bold'>VHDL Answers to Frequently Asked =
> > Questions,
> > 2nd Edition</span></b>, isbn 0-7923-8115<br>
> > ------------------------------------------------------------------------=
> > ------</span></font></p>
> > </div>
> > </div>
> > </body>
> > </html>
> > ------=_NextPart_001_003B_01C42084.9E3CE7A0--
> >
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0
> > Content-Type: message/rfc822
> > Content-Transfer-Encoding: 7bit
> > Content-Disposition: attachment
> >
> > From: <VhdlCohen@aol.com>
> > Sender: <owner-sv-ec@eda.org>
> > To: <john.havlicek@motorola.com>,
> > <krolnik@lsil.com>
> > Cc: <sv-ec@eda.org>
> > Subject: Re: [Fwd: [sv-ec] not (a |->b), not(a |=> b) disallowed?]
> > Date: Sun, 11 Apr 2004 08:53:26 -0700
> > Message-ID: <1e.269724d3.2daac3f6@aol.com>
> > MIME-Version: 1.0
> > Content-Type: multipart/alternative;
> > boundary="----=_NextPart_000_0029_01C42084.9E3805A0"
> > X-Mailer: 9.0 for Windows sub 840
> > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
> > X-Scan-Signature: 62d557eb39c38d1f7066fe03ac633659
> > X-pstn-levels: (S:88.13125/99.87607 R:95.9108 P:95.9108 M:95.5423
> C:98.3836 )
> > X-UIDL: n;~!!Xf?"!=Kb!!&N<"!
> > X-Authentication-Warning: server.eda.org: majordom set sender to
> owner-sv-ec@eda.org using -f
> >
> > This is a multi-part message in MIME format.
> > ------=_NextPart_000_0029_01C42084.9E3805A0
> > Content-Type: text/plain;
> > charset="us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > In a message dated 4/11/2004 8:34:45 AM Pacific Standard Time,
> > john.havlicek@motorola.com writes:
> >
> > I do not agree that these forms should be illegal in SVA. =20
> > They are legal in PSL.
> >
> > You're correct from an LRM viewpoint that they are legal in PSL.
> > However, I know of one tool vendor (I haven't tried others) that will
> > not compile such a structure.=20
> >
> >
> > I agree that their use is generally suspect, so I would=20
> > promote warnings and linting messages to make sure people
> > intend what they are getting with these forms.
> >
> > However, making them illegal complicates the language
> > in ways that I think are not necessary.
> >
> >
> > I'll go along with that. However, a note of caution should be added.=20
> > If vendors do the same thing with the "not" as with the PSL "never" =
> > with
> > an implication operator (i.e., disallow it), then we should modify the
> > example on page 236 to a simple sequence, something like:=20
> > property rule2;
> > @(clkev) disable iff (foo) not a ##1 b ##1 c ##1 d;
> > endproperty"
> > =20
> > Instead of=20
> > LRM 17.11 The property definition states on page 236
> > "This allows for the following examples:
> > ...
> > property rule2;
> > @(clkev) disable iff (foo) not a |-> b ##1 c ##1 d;
> > endproperty"
> > =20
> > ------------------------------------------------------------------------=
> >
> > -----
> > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830=20
> > http://www. <http://www.vhdlcohen.com/> vhdlcohen.com/ =
> > vhdlcohen@aol.com
> >
> > Author of following textbooks:=20
> > * Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004
> > isbn 0-9705394-6-0
> > * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> > 0-9705394-2-8=20
> > * Component Design by Example ", 2001 isbn 0-9705394-0-1
> > * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
> > 0-7923-8474-1
> > * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn
> > 0-7923-8115
> > ------------------------------------------------------------------------=
> >
> > ------
> >
> > ------=_NextPart_000_0029_01C42084.9E3805A0
> > Content-Type: text/html;
> > charset="us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
> > <HTML><HEAD>
> >
> > <META content=3D"MSHTML 6.00.2800.1400" name=3DGENERATOR></HEAD>
> > <BODY id=3Drole_body style=3D"FONT-SIZE: 10pt; COLOR: #000000; =
> > FONT-FAMILY: Arial"=20
> > bottomMargin=3D7 leftMargin=3D7 topMargin=3D7 rightMargin=3D7><FONT =
> > id=3Drole_document=20
> > face=3DArial color=3D#000000 size=3D2>
> > <DIV>
> > <DIV>In a message dated 4/11/2004 8:34:45 AM Pacific Standard Time,=20
> > john.havlicek@motorola.com writes:</DIV>
> > <BLOCKQUOTE=20
> > style=3D"PADDING-LEFT: 5px; MARGIN-LEFT: 5px; BORDER-LEFT: blue 2px =
> > solid"><FONT=20
> > style=3D"BACKGROUND-COLOR: transparent" face=3DArial color=3D#000000 =
> > size=3D2>I do not=20
> > agree that these forms should be illegal in SVA.  <BR>They are =
> > legal in=20
> > PSL.</FONT></BLOCKQUOTE>
> > <DIV>You're correct from an LRM viewpoint that they are legal in =
> > PSL. =20
> > However,  I know of one tool vendor (I haven't tried others) that =
> > will not=20
> > compile such a structure. </DIV>
> > <BLOCKQUOTE=20
> > style=3D"PADDING-LEFT: 5px; MARGIN-LEFT: 5px; BORDER-LEFT: blue 2px =
> > solid"><FONT=20
> > style=3D"BACKGROUND-COLOR: transparent" face=3DArial color=3D#000000 =
> > size=3D2><BR>I=20
> > agree that their use is generally suspect, so I would <BR>promote =
> > warnings and=20
> > linting messages to make sure people<BR>intend what they are getting =
> > with=20
> > these forms.<BR><BR>However, making them illegal complicates the=20
> > language<BR>in ways that I think are not =
> > necessary.<BR></FONT></BLOCKQUOTE>
> > <DIV>I'll go along with that.  However, a note of caution should =
> > be added.=20
> > </DIV>
> > <DIV>If vendors do the same thing with the "not" as with the PSL =
> > "never" with an=20
> > implication operator (i.e., disallow it), then we should modify the =
> > example on=20
> > page 236 to a simple sequence, something like: </DIV>
> > <DIV>
> > <DIV>property rule2;<BR>     @(clkev) disable iff =
> > (foo) not=20
> > a ##1 b ##1 c ##1 d;<BR>endproperty"</DIV></DIV>
> > <DIV> </DIV>
> > <DIV>Instead of </DIV>
> > <DIV>
> > <DIV>LRM 17.11 The property definition   states on page =
> > 236</DIV>
> > <DIV>"This allows for the following examples:<BR>...</DIV>
> > <DIV>property rule2;<BR>     @(clkev) disable iff =
> > (foo) not=20
> > a |-> b ##1 c ##1 d;<BR>endproperty"</DIV></DIV></DIV>
> > <DIV> </DIV>
> > <DIV><FONT lang=3D0 face=3DArial size=3D1 FAMILY=3D"SANSSERIF"=20
> > PTSIZE=3D"8">-----------------------------------------------------------=
> > ------------------<BR>Ben=20
> > Cohen Trainer, Consultant, Publisher (310) 721-4830 <BR><A=20
> > href=3D"http://www.vhdlcohen.com/">http://www.<B>vhdlcohen</B>.com/</A> =
> >
> > vhdlcohen@aol.com <BR>Author of following textbooks: <BR>* <B>Using =
> > PSL/SUGAR=20
> > for Formal and Dynamic Verification 2nd Edition, </B>2004 isbn=20
> > 0-9705394-6-0<BR>* <B>Real Chip Design and Verification Using Verilog =
> > and=20
> > VHDL</B>, 2002 isbn 0-9705394-2-8 <BR>* <B>Component Design by =
> > Example</B> ",=20
> > 2001 isbn 0-9705394-0-1<BR>* <B>VHDL Coding Styles and Methodologies, =
> > 2nd=20
> > Edition</B>, 1999 isbn 0-7923-8474-1<BR>* <B>VHDL Answers to Frequently =
> > Asked=20
> > Questions, 2nd Edition</B>, isbn=20
> > 0-7923-8115<BR>---------------------------------------------------------=
> > ---------------------</FONT></DIV></FONT></BODY></HTML>
> > ------=_NextPart_000_0029_01C42084.9E3805A0--
> >
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0
> > Content-Type: message/rfc822
> > Content-Transfer-Encoding: 7bit
> > Content-Disposition: attachment
> >
> > From: "Adam Krolnik" <krolnik@lsil.com>
> > To: <VhdlCohen@aol.com>
> > Cc: <David.Smith@Synopsys.COM>,
> > <sv-ec@eda.org>,
> > <sri@noveldv.com>,
> > <sv-ac@eda.org>
> > References: <7e.4ba287e6.2daa3326@aol.com>
> > Subject: Re: [sv-ec] not (a |->b), not(a |=> b) disallowed?
> > Date: Mon, 12 Apr 2004 07:52:07 -0700
> > Message-ID: <407AAD17.3050401@lsil.com>
> > MIME-Version: 1.0
> > Content-Type: multipart/alternative;
> > boundary="----=_NextPart_000_002D_01C42084.9E3805A0"
> > X-Mailer: Microsoft Outlook, Build 10.0.6626
> > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
> > X-pstn-levels: (S:99.90000/99.90000 R:95.9108 P:95.9108 M:98.8113
> C:78.1961 )
> > X-pstn-settings: 1 (0.1500:0.1500) r p m C
> > X-pstn-addresses: from <krolnik@lsil.com> [48/2]
> > X-UIDL: ;oU!!>cM"!>j7!!!W-"!
> > In-Reply-To: <7e.4ba287e6.2daa3326@aol.com>
> > X-Accept-Language: en-us, en
> > X-Scanned-By: MIMEDefang 2.39
> >
> > This is a multi-part message in MIME format.
> > ------=_NextPart_000_002D_01C42084.9E3805A0
> > Content-Type: text/plain;
> > charset="us-ascii"
> > Content-Transfer-Encoding: 7bit
> >
> >
> >
> > Hi Ben;
> >
> > The LRM example you show
> >
> > >LRM 17.11 The property definition states on page 236
> > >property rule2;
> > > @(clkev) disable iff (foo) not a |-> b ##1 c ##1 d;
> > >endproperty"
> >
> > Hmmm, I thought we were going to drop the "not" from this example - or
> > was it another?
> >
> >
> > There is one other problem with this property. It suffers from incorrect
> > precedence
> > assumption. It is really parsed as:
> >
> >
> > (not a) |-> b ##1 c ##1 d
> >
> > Since the operator 'not' has highest precedence (over implication) you
> > don't really get
> > what you may want (maybe twice).
> >
> >
> > Adam Krolnik
> > Verification Mgr.
> > LSI Logic Corp.
> > Plano TX. 75074
> > Co-author "Assertion-Based Design"
> >
> >
> >
> > ------=_NextPart_000_002D_01C42084.9E3805A0
> > 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.4630.0">
> > <TITLE>Re: [sv-ec] not (a |->b), not(a |=3D> b) =
> > disallowed?</TITLE>
> > </HEAD>
> > <BODY>
> > 
> > <BR>
> > <BR>
> > <P><FONT SIZE=3D2>Hi Ben;</FONT>
> > </P>
> > <P><FONT SIZE=3D2>The LRM example you show</FONT>
> > </P>
> > <P><FONT SIZE=3D2> >LRM 17.11 The property =
> > definition   states on page 236</FONT>
> > <BR><FONT SIZE=3D2> >property rule2;</FONT>
> > <BR><FONT SIZE=3D2> >     @(clkev) disable =
> > iff (foo) not a |-> b ##1 c ##1 d;</FONT>
> > <BR><FONT SIZE=3D2> >endproperty"</FONT>
> > </P>
> > <P><FONT SIZE=3D2>Hmmm, I thought we were going to drop the =
> > "not" from this example - or was it another?</FONT>
> > </P>
> > <BR>
> > <P><FONT SIZE=3D2>There is one other problem with this property. It =
> > suffers from incorrect precedence </FONT>
> > <BR><FONT SIZE=3D2>assumption. It is really parsed as:</FONT>
> > </P>
> > <BR>
> > <P><FONT SIZE=3D2>(not a) |-> b ##1 c ##1 d</FONT>
> > </P>
> > <P><FONT SIZE=3D2>Since the operator 'not' has highest precedence (over =
> > implication) you don't really get</FONT>
> > <BR><FONT SIZE=3D2>what you may want (maybe twice).</FONT>
> > </P>
> > <BR>
> > <P><FONT SIZE=3D2>    Adam Krolnik</FONT>
> > <BR><FONT SIZE=3D2>    Verification Mgr.</FONT>
> > <BR><FONT SIZE=3D2>    LSI Logic Corp.</FONT>
> > <BR><FONT SIZE=3D2>    Plano TX. 75074</FONT>
> > <BR><FONT SIZE=3D2>    Co-author "Assertion-Based =
> > Design"</FONT>
> > </P>
> > <BR>
> > </BODY>
> > </HTML>
> > ------=_NextPart_000_002D_01C42084.9E3805A0--
> >
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0
> > Content-Type: message/rfc822
> > Content-Transfer-Encoding: 7bit
> > Content-Disposition: attachment
> >
> > From: <VhdlCohen@aol.com>
> > To: <David.Smith@Synopsys.COM>,
> > <sv-ec@eda.org>
> > Cc: <sri@noveldv.com>
> > Subject: Re: [sv-ec] not (a |->b), not(a |=> b) disallowed?
> > Date: Sat, 10 Apr 2004 22:35:34 -0700
> > Message-ID: <7e.4ba287e6.2daa3326@aol.com>
> > MIME-Version: 1.0
> > Content-Type: multipart/alternative;
> > boundary="----=_NextPart_000_0031_01C42084.9E3A76A0"
> > X-Mailer: 9.0 for Windows sub 840
> > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
> > X-pstn-levels: (S:33.09916/99.41902 R:95.9108 P:95.9108 M:99.8514
> C:78.1961 )
> > X-pstn-settings: 1 (0.1500:0.1500) r p m C
> > X-pstn-addresses: from <VhdlCohen@aol.com> [48/2]
> > X-UIDL: n8e"!m+^"!Inp!!6j-!!
> >
> > This is a multi-part message in MIME format.
> > ------=_NextPart_000_0031_01C42084.9E3A76A0
> > Content-Type: text/plain;
> > charset="us-ascii"
> > Content-Transfer-Encoding: 7bit
> >
> > LRM 17.11 The property definition states on page 236
> > "This allows for the following examples:
> > ...
> > property rule2;
> > @(clkev) disable iff (foo) not a |-> b ##1 c ##1 d;
> > endproperty"
> >
> > That implies that the LRM blesses the structure "not a |-> b"
> > I still believe that this should not be allowed, per my previous email,
> > because if
> > "a" is false, then the property expression "a |-> b" is true, and the
> > property is false, or fails.
> > The way it stands, per LRM "not a |-> b" has the following meaning:
> > a b a|-> b not a|-> b
> > 0 0 true false
> > 0 1 true false
> > 1 0 false true
> > 1 1 true false
> >
> > Thus, "not a |-> b", is same as a |-> !b
> > and is not the same meaning as "! (a && b)
> >
> > The way the definition stand, the implication operator with the "not" is
> > very confusing.
> > On the surface "not a |-> b" does not look like it means a |-> !b.
> > This gets even more confusing when you have a cascade of implication
> > operators, like
> > not a |-> b |-> c |->d
> >
> > I recommend that the committee re-examines the legality and application
> > of this property expression.
> >
> >
> >
> > In a message dated 4/9/2004 3:06:45 PM Pacific Standard Time,
> > VhdlCohen@aol.com writes:
> >
> >
> > The following property expressions should be disallowed in the LRM:
> > not (a |->b), // by "a" or "b" I mean the sequences "a" "b"
> > not(a |=> b)
> > Rationale: from FROM LRM: 17.11.1 Implication
> > "If there is no match of the antecedent sequence_expr from a given
> > start point, then evaluation of the implication
> > from that start point succeeds vacuously and returns true"
> > Thus, is "a" is false, (a |-> b) or (a |=>b) become TRUE, and "not(a
> > |-> b)" or "not(a |=>b)" becomes FALSE, or failure.
> > That is not the intent here.
> > In PSL, we disallow a "never {a} |-> {b}" or "never {a} |=> {b}"
> >
> > By the way, one could express the never implication with sequences as:
> > (a |-> b |-> 'false)
> > Ben
> >
> >
> > ------------------------------------------------------------------------
> > -----
> > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
> > http://www. <http://www.vhdlcohen.com/> vhdlcohen.com/ vhdlcohen@aol.com
> >
> > Author of following textbooks:
> > * Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004
> > isbn 0-9705394-6-0
> > * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> > 0-9705394-2-8
> > * Component Design by Example ", 2001 isbn 0-9705394-0-1
> > * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
> > 0-7923-8474-1
> > * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn
> > 0-7923-8115
> > ------------------------------------------------------------------------
> > ------
> >
> > ------=_NextPart_000_0031_01C42084.9E3A76A0
> > Content-Type: text/html;
> > charset="us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
> > <HTML><HEAD>
> >
> > <META content=3D"MSHTML 6.00.2800.1400" name=3DGENERATOR></HEAD>
> > <BODY id=3Drole_body style=3D"FONT-SIZE: 10pt; COLOR: #000000; =
> > FONT-FAMILY: Arial"=20
> > bottomMargin=3D7 leftMargin=3D7 topMargin=3D7 rightMargin=3D7><FONT =
> > id=3Drole_document=20
> > face=3DArial color=3D#000000 size=3D2>
> > <DIV>
> > <DIV>
> > <DIV>LRM 17.11 The property definition   states on page =
> > 236</DIV>
> > <DIV>"This allows for the following examples:<BR>...</DIV>
> > <DIV>property rule2;<BR>     @(clkev) disable iff =
> > (foo) not=20
> > a |-> b ##1 c ##1 d;<BR>endproperty"</DIV>
> > <DIV> </DIV>
> > <DIV>That implies that the LRM blesses the structure "not a |-> =
> > b"</DIV>
> > <DIV>I still believe that this should not be allowed, per my previous =
> > email,=20
> > because if </DIV>
> > <DIV>"a" is false, then the property expression "a |-> b" is true, =
> > and the=20
> > property is false, or fails. </DIV>
> > <DIV>The way it stands, per LRM "not a |-> b" has the following=20
> > meaning:</DIV>
> > <DIV><FONT face=3D"Courier New">a  b     =
> > a|->=20
> > b   not a|-> b</FONT></DIV>
> > <DIV><FONT face=3D"Courier New">0 =20
> > 0      true    =20
> > false</FONT></DIV>
> > <DIV><FONT face=3D"Courier New">0  1      =
> >
> > true     false</FONT></DIV>
> > <DIV><FONT face=3D"Courier New">1 =20
> > 0      false    =
> > true</FONT></DIV>
> > <DIV><FONT face=3D"Courier New">1 =20
> > 1      true     f=
> > alse</FONT></DIV>
> > <DIV> </DIV>
> > <DIV>Thus, "not a |-> b", is same as  a |-> !b </DIV>
> > <DIV>and is not the same meaning as   "! (a && b) =
> > </DIV>
> > <DIV>
> > <DIV><FONT face=3D"Courier New"></FONT> </DIV>
> > <DIV>The way the definition stand, the implication operator with the =
> > "not" is=20
> > very confusing. </DIV>
> > <DIV>On the surface "not a |-> b" does not look like it means a =
> > |->=20
> > !b.</DIV>
> > <DIV>This gets even more confusing when you have a cascade of =
> >  implication=20
> > operators, like </DIV>
> > <DIV>  not a |-> b |-> c |->d </DIV>
> > <DIV> </DIV>
> > <DIV>I recommend that the committee re-examines the legality and =
> > application of=20
> > this property expression.  </DIV></DIV>
> > <DIV> </DIV>
> > <DIV> </DIV>
> > <DIV> </DIV>
> > <DIV>In a message dated 4/9/2004 3:06:45 PM Pacific Standard Time,=20
> > VhdlCohen@aol.com writes:</DIV>
> > <BLOCKQUOTE=20
> > style=3D"PADDING-LEFT: 5px; MARGIN-LEFT: 5px; BORDER-LEFT: blue 2px =
> > solid"><FONT=20
> > style=3D"BACKGROUND-COLOR: transparent" face=3DArial color=3D#000000 =
> > size=3D2><FONT=20
> > face=3DArial color=3D#000000 size=3D2>
> > <DIV>The following property expressions should be disallowed in the =
> > LRM:=20
> > </DIV>
> > <DIV><STRONG>not (a |->b),</STRONG>   // by "a" or =
> > "b" I=20
> > mean the sequences "a" "b"</DIV>
> > <DIV><STRONG>not(a |=3D> b)</STRONG>  </DIV>
> > <DIV>Rationale:   from <SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">FROM LRM: =
> > 17.11.1=20
> > Implication<BR></SPAN><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">  "If =
> > there is no=20
> > match</SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">=20
> > </SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">of the =
> > antecedent=20
> > sequence</SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: =
> > Arial">_</SPAN></STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">expr from =
> > a given=20
> > start point, then evaluation of the implication<BR>from that start =
> > point=20
> > succeeds vacuously </SPAN><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">and returns =
> > true"=20
> > </SPAN></STRONG></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>Thus, is "a" is false,  <STRONG>(a |-> =
> > b)</STRONG> or=20
> > <STRONG>(a |=3D>b)</STRONG> become TRUE, and "<STRONG>not(a |-> =
> >
> > b</STRONG>)" or <STRONG>"not(a |=3D>b)"</STRONG>  becomes =
> > FALSE, or=20
> > failure. </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>That is not the intent here.  =
> > </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>In PSL, we disallow a <STRONG>"never {a} |-> {b}"=20
> > </STRONG>or<STRONG> "never {a} |=3D> =
> > {b}"</STRONG></FONT></SPAN></DIV>
> > <DIV><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><STRONG><FONT=20
> > color=3D#000000></FONT></STRONG></SPAN> </DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>By the way, one could express the never implication =
> > with=20
> > sequences as: </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000> (a |-> b |-> 'false)</FONT></SPAN></DIV>
> > <DIV><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><STRONG><FONT=20
> > =
> > color=3D#000000>Ben</FONT></STRONG></SPAN></DIV></FONT></FONT></BLOCKQUO=
> > TE></DIV>
> > <DIV></DIV></DIV>
> > <DIV> </DIV>
> > <DIV><FONT lang=3D0 face=3DArial size=3D1 FAMILY=3D"SANSSERIF"=20
> > PTSIZE=3D"8">-----------------------------------------------------------=
> > ------------------<BR>Ben=20
> > Cohen Trainer, Consultant, Publisher (310) 721-4830 <BR><A=20
> > href=3D"http://www.vhdlcohen.com/">http://www.<B>vhdlcohen</B>.com/</A> =
> >
> > vhdlcohen@aol.com <BR>Author of following textbooks: <BR>* <B>Using =
> > PSL/SUGAR=20
> > for Formal and Dynamic Verification 2nd Edition, </B>2004 isbn=20
> > 0-9705394-6-0<BR>* <B>Real Chip Design and Verification Using Verilog =
> > and=20
> > VHDL</B>, 2002 isbn 0-9705394-2-8 <BR>* <B>Component Design by =
> > Example</B> ",=20
> > 2001 isbn 0-9705394-0-1<BR>* <B>VHDL Coding Styles and Methodologies, =
> > 2nd=20
> > Edition</B>, 1999 isbn 0-7923-8474-1<BR>* <B>VHDL Answers to Frequently =
> > Asked=20
> > Questions, 2nd Edition</B>, isbn=20
> > 0-7923-8115<BR>---------------------------------------------------------=
> > ---------------------</FONT></DIV></FONT></BODY></HTML>
> > ------=_NextPart_000_0031_01C42084.9E3A76A0--
> >
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0
> > Content-Type: message/rfc822
> > Content-Transfer-Encoding: 7bit
> > Content-Disposition: attachment
> >
> > From: <VhdlCohen@aol.com>
> > Sender: <owner-sv-ec@eda.org>
> > To: <David.Smith@Synopsys.COM>,
> > <sv-ec@eda.org>
> > Cc: <sri@noveldv.com>
> > Subject: [sv-ec] not (a |->b), not(a |=> b) disallowed?
> > Date: Fri, 9 Apr 2004 15:04:14 -0700
> > Message-ID: <ce.4a68b9d9.2da877de@aol.com>
> > MIME-Version: 1.0
> > Content-Type: multipart/alternative;
> > boundary="----=_NextPart_000_0035_01C42084.9E3CE7A0"
> > X-Mailer: 9.0 for Windows sub 840
> > X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
> > X-Scan-Signature: 36e365df5a532e5e672ad9dec1ca2d66
> > X-pstn-levels: (S:34.43163/99.43468 R:95.9108 P:95.9108 M:99.8514
> C:78.1961 )
> > X-UIDL: paG"!+?<!!H,="!iKO!!
> > X-Authentication-Warning: server.eda.org: majordom set sender to
> owner-sv-ec@eda.org using -f
> >
> > This is a multi-part message in MIME format.
> > ------=_NextPart_000_0035_01C42084.9E3CE7A0
> > Content-Type: text/plain;
> > charset="us-ascii"
> > Content-Transfer-Encoding: 7bit
> >
> > The following property expressions should be disallowed in the LRM:
> > not (a |->b), // by "a" or "b" I mean the sequences "a" "b"
> > not(a |=> b)
> > Rationale: from FROM LRM: 17.11.1 Implication
> > "If there is no match of the antecedent sequence_expr from a given
> > start point, then evaluation of the implication
> > from that start point succeeds vacuously and returns true"
> > Thus, is "a" is false, (a |-> b) or (a |=>b) become TRUE, and "not(a
> > |-> b)" or "not(a |=>b)" becomes FALSE, or failure.
> > That is not the intent here.
> > In PSL, we disallow a "never {a} |-> {b}" or "never {a} |=> {b}"
> >
> > By the way, one could express the never implication with sequences as:
> > (a |-> b |-> 'false)
> > Ben
> >
> >
> > ------------------------------------------------------------------------
> > -----
> > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
> > http://www. <http://www.vhdlcohen.com/> vhdlcohen.com/ vhdlcohen@aol.com
> >
> > Author of following textbooks:
> > * Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004
> > isbn 0-9705394-6-0
> > * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> > 0-9705394-2-8
> > * Component Design by Example ", 2001 isbn 0-9705394-0-1
> > * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
> > 0-7923-8474-1
> > * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn
> > 0-7923-8115
> > ------------------------------------------------------------------------
> > ------
> >
> >
> > ------=_NextPart_000_0035_01C42084.9E3CE7A0
> > Content-Type: text/html;
> > charset="us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
> > <HTML><HEAD>
> >
> > <META content=3D"MSHTML 6.00.2800.1400" name=3DGENERATOR></HEAD>
> > <BODY id=3Drole_body style=3D"FONT-SIZE: 10pt; COLOR: #000000; =
> > FONT-FAMILY: Arial"=20
> > bottomMargin=3D7 leftMargin=3D7 topMargin=3D7 rightMargin=3D7><FONT =
> > id=3Drole_document=20
> > face=3DArial color=3D#000000 size=3D2>
> > <DIV>The following property expressions should be disallowed in the =
> > LRM: </DIV>
> > <DIV><STRONG>not (a |->b),</STRONG>   // by "a" or =
> > "b" I=20
> > mean the sequences "a" "b"</DIV>
> > <DIV><STRONG>not(a |=3D> b)</STRONG>  </DIV>
> > <DIV>Rationale:   from <SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">FROM LRM: =
> > 17.11.1=20
> > Implication<BR></SPAN><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">  "If =
> > there is no=20
> > match</SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">=20
> > </SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">of the =
> > antecedent=20
> > sequence</SPAN></STRONG><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: =
> > Arial">_</SPAN></STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">expr from a =
> > given=20
> > start point, then evaluation of the implication<BR>from that start =
> > point succeeds vacuously </SPAN><STRONG><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: Arial">and returns =
> > true"=20
> > </SPAN></STRONG></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>Thus, is "a" is false,  <STRONG>(a |-> =
> > b)</STRONG> or=20
> > <STRONG>(a |=3D>b)</STRONG> become TRUE, and "<STRONG>not(a |-> =
> > b</STRONG>)"=20
> > or <STRONG>"not(a |=3D>b)"</STRONG>  becomes FALSE, or failure. =
> >
> > </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>That is not the intent here.  </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>In PSL, we disallow a <STRONG>"never {a} |-> {b}"=20
> > </STRONG>or<STRONG> "never {a} |=3D> =
> > {b}"</STRONG></FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><STRONG><FONT=20
> > color=3D#000000></FONT></STRONG></SPAN> </DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000>By the way, one could express the never implication =
> > with sequences=20
> > as: </FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><FONT=20
> > color=3D#000000> (a |-> b |-> 'false)</FONT></SPAN></DIV>
> > <DIV><SPAN style=3D"FONT-SIZE: 10pt; COLOR: red; FONT-FAMILY: =
> > Arial"><STRONG><FONT=20
> > color=3D#000000>Ben</FONT></STRONG></SPAN></DIV>
> > <DIV>
> > <P class=3DMsoNormal style=3D"MARGIN: 0in 0in 0pt"><SPAN=20
> > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: =
> > Arial"> </SPAN><FONT=20
> > lang=3D0 face=3DArial size=3D1 FAMILY=3D"SANSSERIF"=20
> > PTSIZE=3D"8">-----------------------------------------------------------=
> > ------------------<BR>Ben=20
> > Cohen Trainer, Consultant, Publisher (310) 721-4830 <BR><A=20
> > href=3D"http://www.vhdlcohen.com/">http://www.<B>vhdlcohen</B>.com/</A> =
> >
> > vhdlcohen@aol.com <BR>Author of following textbooks: <BR>* <B>Using =
> > PSL/SUGAR=20
> > for Formal and Dynamic Verification 2nd Edition, </B>2004 isbn=20
> > 0-9705394-6-0<BR>* <B>Real Chip Design and Verification Using Verilog =
> > and=20
> > VHDL</B>, 2002 isbn 0-9705394-2-8 <BR>* <B>Component Design by =
> > Example</B> ",=20
> > 2001 isbn 0-9705394-0-1<BR>* <B>VHDL Coding Styles and Methodologies, =
> > 2nd=20
> > Edition</B>, 1999 isbn 0-7923-8474-1<BR>* <B>VHDL Answers to Frequently =
> > Asked=20
> > Questions, 2nd Edition</B>, isbn=20
> > 0-7923-8115<BR>---------------------------------------------------------=
> > ---------------------</FONT></P></DIV></FONT></BODY></HTML>
> > ------=_NextPart_000_0035_01C42084.9E3CE7A0--
> >
> > ------=_NextPart_000_003A_01C42084.9E3CE7A0--

**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752

Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
Received on Tue Apr 13 07:36:41 2004

This archive was generated by hypermail 2.1.8 : Tue Apr 13 2004 - 07:36:43 PDT

Re: [sv-ac] FW: [sv-ec] not (a |->b), not(a |=> b) disallowed?