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

From: John Havlicek <john.havlicek@motorola.com>
Date: Mon Apr 12 2004 - 20:46:28 PDT

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--
Received on Mon Apr 12 20:46:37 2004

This archive was generated by hypermail 2.1.8 : Mon Apr 12 2004 - 20:46:48 PDT

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