Hi Ben: You make a very good point. The LRM does not have a real definition of the distinction of "vacuous" from "non-vacuous" success. My opinion is that it may be useful to consider successes that result from satisfaction the "disable iff" as yet another category in the partition. In other words, to separate the vacuous successes that result from failure to match the antecedent of an implication, but which are not terminated by a "disable iff", from successes that are terminated by a "disable iff". In the presence of nested implication operators, I think "non-vacuous" success should require that all nested antecedents match. Such a convention has the nice property that the notion of "non-vacuous" success is the same for pairs such as S |=> (T |-> U) and (S ##1 T) |-> U that are related by adjointness. Best regards, John H. > Content-class: urn:content-classes:message > x-mimeole: Produced By Microsoft Exchange V6.5.7226.0 > x-aol-ip: 64.12.136.44 > x-authentication-warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f > x-mb-message-source: WebUI > x-mb-message-type: User > x-spam-flag: NO > x-virus-status: Clean > Date: Thu, 18 Aug 2005 21:20:06 -0700 > X-MS-Has-Attach: > X-MS-TNEF-Correlator: > Thread-Topic: [sv-ac] Is result of disable iff (true_expression) vacuous or true success? > Thread-Index: AcWkdk7jqq6kZL//TVusUzBGX4WxTg== > From: <vhdlcohen@aol.com> > Sender: <owner-sv-ac@eda.org> > > This is a multi-part message in MIME format. > > ------_=_NextPart_001_01C5A476.4E7F7800 > Content-Type: text/plain; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > IEEE P1800/D5 and SV 3.1a LRM 17.11 is unclear on this issue. LRM=20 > states "If prior to the completion of that evaluation the reset=20 > expression becomes true, then the overall evaluation of the=20 > property_spec is true." > But a true evaluation can be considered as success, which is not=20 > really the correct interpretation of a reset of an assertion. If fact,=20 > in PSL an abort, which is equivalent to a SVA disable, causes an=20 > "immediate termination of current and future obligations of a property. > > The problem is that a tool vendor can interpret a disable iff=20 > (true_expression) as success or as vacuous success. That issue needs=20 > clarification. I suggest that we clarify the LRM to state something=20 > like ""If prior to the completion of that evaluation the reset=20 > expression becomes true, then the overall evaluation of the=20 > property_spec is true, and is considered a vacuous success". > Ben > =20 > ------------------------------------------------------------------------ > -- > Ben Cohen Trainer, Consultant, Publisher (310) 721-4830 > http://www.vhdlcohen.com/ ben_ f rom _abv-sva.org > * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9 > * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd=20 > Edition, 2004, ISBN 0-9705394-6-0 > * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn=20 > 0-9705394-2-8 > * Component Design by Example ", 2001 isbn 0-9705394-0-1 > * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn=20 > 0-7923-8474-1 > * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn=20 > 0-7923-8115 > =20 > ------------------------------------------------------------------------ > --------- > > ------_=_NextPart_001_01C5A476.4E7F7800 > Content-Type: text/html; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN"> > <HTML> > <HEAD> > <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; = > charset=3Dus-ascii"> > <META NAME=3D"Generator" CONTENT=3D"MS Exchange Server version = > 6.5.7232.36"> > <TITLE>[sv-ac] Is result of disable iff (true_expression) vacuous or = > true success? </TITLE> > </HEAD> > <BODY> > <!-- Converted from text/plain format --> > > <P><FONT SIZE=3D2>IEEE P1800/D5 and SV 3.1a LRM 17.11 is unclear on this = > issue. LRM </FONT> > > <BR><FONT SIZE=3D2>states "If prior to the completion of that = > evaluation the reset </FONT> > > <BR><FONT SIZE=3D2>expression becomes true, then the overall evaluation = > of the </FONT> > > <BR><FONT SIZE=3D2>property_spec is true."</FONT> > > <BR><FONT SIZE=3D2> But a true evaluation can be considered as = > success, which is not </FONT> > > <BR><FONT SIZE=3D2>really the correct interpretation of a reset of an = > assertion. If fact, </FONT> > > <BR><FONT SIZE=3D2>in PSL an abort, which is equivalent to a SVA = > disable, causes an </FONT> > > <BR><FONT SIZE=3D2>"immediate termination of current and future = > obligations of a property.</FONT> > </P> > > <P><FONT SIZE=3D2> The problem is that a tool vendor can interpret = > a disable iff </FONT> > > <BR><FONT SIZE=3D2>(true_expression) as success or as vacuous success. = > That issue needs </FONT> > > <BR><FONT SIZE=3D2>clarification. I suggest that we clarify the = > LRM to state something </FONT> > > <BR><FONT SIZE=3D2>like ""If prior to the completion of that = > evaluation the reset </FONT> > > <BR><FONT SIZE=3D2>expression becomes true, then the overall evaluation = > of the </FONT> > > <BR><FONT SIZE=3D2>property_spec is true, and is considered a vacuous = > success".</FONT> > > <BR><FONT SIZE=3D2> Ben</FONT> > > <BR><FONT SIZE=3D2> </FONT> > > <BR><FONT = > SIZE=3D2>----------------------------------------------------------------= > ----------</FONT> > > <BR><FONT SIZE=3D2> Ben Cohen Trainer, Consultant, Publisher (310) = > 721-4830</FONT> > > <BR><FONT SIZE=3D2> <A = > HREF=3D"http://www.vhdlcohen.com/">http://www.vhdlcohen.com/</A> = > ben@abv-sva.org</FONT> > > <BR><FONT SIZE=3D2> * Co-Author: SystemVerilog Assertions Handbook, = > 2005 ISBN 0-9705394-7-9</FONT> > > <BR><FONT SIZE=3D2> * Co-Author: Using PSL/SUGAR for Formal and = > Dynamic Verification 2nd </FONT> > > <BR><FONT SIZE=3D2>Edition, 2004, ISBN 0-9705394-6-0</FONT> > > <BR><FONT SIZE=3D2> * Real Chip Design and Verification Using = > Verilog and VHDL, 2002 isbn </FONT> > > <BR><FONT SIZE=3D2>0-9705394-2-8</FONT> > > <BR><FONT SIZE=3D2> * Component Design by Example ", 2001 isbn = > 0-9705394-0-1</FONT> > > <BR><FONT SIZE=3D2> * VHDL Coding Styles and Methodologies, 2nd = > Edition, 1999 isbn </FONT> > > <BR><FONT SIZE=3D2>0-7923-8474-1</FONT> > > <BR><FONT SIZE=3D2> * VHDL Answers to Frequently Asked Questions, = > 2nd Edition, isbn </FONT> > > <BR><FONT SIZE=3D2>0-7923-8115</FONT> > > <BR><FONT SIZE=3D2> </FONT> > > <BR><FONT = > SIZE=3D2>----------------------------------------------------------------= > -----------------</FONT> > </P> > > </BODY> > </HTML> > ------_=_NextPart_001_01C5A476.4E7F7800--Received on Fri Aug 19 07:27:58 2005
This archive was generated by hypermail 2.1.8 : Fri Aug 19 2005 - 07:29:18 PDT