Re: [sv-ac] Is result of disable iff (true_expression) vacuous or true success?

Cindy:

> which is it?

My answer is "both".

But you can judge this for yourself.  

P1800-draft5_prelim5_SystemVerilog_LRM.pdf has the following to say
about the strings "vacuous" and "vacuity" (exclusive of references in 
the index):

Section 17.11.2, p. 257:

  - 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.

Section 17.13.3, p. 276:

  The results of coverage statement for a property shall contain:
  
  - Number of times attempted
  - Number of times succeeded
  - Number of times failed
  - Number of times succeeded because of vacuity
  
  In addition, statement_or_null is executed every time a property succeeds.
  
  Vacuity rules are applied only when implication operator is used.  A property 
  succeeds non-vacuously only if the consequent of the implication contributes 
  to the success.

Section 29.4.3, p. 482:

    vpi_get(vpiAssertSuccessCovered, assertion_handle)
  
  Returns the number of times the assertion has succeeded non-vacuously or, if 
  assertion handle corresponds to a cover sequence, the number of times the 
  sequence has been matched.  Refer to 17.11.2 and 17.13 for the definition of 
  vacuity.
  
    vpi_get(vpiAssertVacuousSuccessCovered, assertion_handle)
  
  Returns the number of times the assertion has succeeded vacuously.  Refer to 17.11.2 
  and 17.13 for the definition of vacuity.
  
  ...
  
  For any assertion, the number of attempts that have not yet reached any conclusion
  (success or failure) can be derived from the formula:
  
    in progress = attempts - (successes + vacuous success + failures)


Best regards,

John H.




























> Content-class: urn:content-classes:message
> x-mimeole: Produced By Microsoft Exchange V6.5.7226.0
> x-mimetrack: Serialize by Router on D12ML102/12/M/IBM(Release 6.5.1| March 5, 2004) at 30/08/2005 14:15:26
> Date: Tue, 30 Aug 2005 04:11:52 -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: AcWtVCVXhRFRRpHZS72c/BuU2F/hTw==
> From: "Cindy Eisner" <EISNER@il.ibm.com>
> Cc: "Havlicek John-r8aaau" <john.havlicek@freescale.com>,
> 	<vhdlcohen@aol.com>,
> 	<sv-ac@eda.org>
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C5AD54.2506FC00
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> 
> 
> 
> 
> manisha, john,
> 
> manisha says "As per current LRM, the 'and' operator never returns
> vacuous
> success."  but john says "The LRM does not have a real definition of the
> distinction of 'vacuous' from 'non-vacuous' success."
> 
> which is it?
> 
> cindy.
> 
> --------------------------------------------------------------------
> Cindy Eisner
> Reliable Systems Technologies
> 
> IBM Haifa Research Lab, 4th floor
> Haifa University Campus
> Haifa 31905, Israel
> Tel: +972-4-8296-266
> Fax: +972-4-8296-114
> e-mail:  eisner@il.ibm.com
> 
> 
> "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com>@eda.org on
> 20/08/2005 00:06:38
> 
> Sent by:    owner-sv-ac@eda.org
> 
> 
> To:    <john.havlicek@freescale.com>, <vhdlcohen@aol.com>
> cc:    <sv-ac@eda.org>
> Subject:    RE: [sv-ac] Is result of disable iff (true_expression)
> vacuous
>        or true success?
> 
> 
> Hi All,
> 
> I like the idea of treating success due to "disable iff" in another
> category separate from vacuous success. But this will require more
> changes in the LRM rather than just fixing the section on "disable iff".
> 
> BTW, I have one question on the vacuous matches due to implication.
> Consider the following example:
>  (a |=3D> b) and (c |=3D> d)
> 
> As per current LRM, the "and" operator never returns vacuous success.
> But if both left and right side of "and" return vacuous successes,
> shouldn't the whole thing be a vacuous success ? And what about only one
> of them returns vacuous success ?
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
> Havlicek
> Sent: Friday, August 19, 2005 7:28 AM
> To: vhdlcohen@aol.com
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] Is result of disable iff (true_expression) vacuous
> or true success?
> 
> 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 |=3D> (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=3D=3D
> > From: <vhdlcohen@aol.com>
> > Sender: <owner-sv-ac@eda.org>
> >
> > This is a multi-part message in MIME format.
> >
> > ------_=3D_NextPart_001_01C5A476.4E7F7800
> > Content-Type: text/plain;
> >            charset=3D"us-ascii"
> > Content-Transfer-Encoding: quoted-printable
> >
> > IEEE P1800/D5 and SV 3.1a LRM 17.11 is unclear on this issue. LRM=3D20
> > states "If prior to the completion of that evaluation the reset=3D20
> > expression becomes true, then the overall evaluation of the=3D20
> > property_spec is true."
> >   But a true evaluation can be considered as success, which is =
> not=3D20
> > really the correct interpretation of a reset of an assertion. If
> > fact,=3D20 in PSL an abort, which is equivalent to a SVA disable, =
> causes
> 
> > an=3D20 "immediate termination of current and future obligations of a
> property.
> >
> >   The problem is that a tool vendor can interpret a disable iff=3D20
> > (true_expression) as success or as vacuous success. That issue
> > needs=3D20 clarification.  I suggest that we clarify the LRM to state
> > something=3D20 like ""If prior to the completion of that evaluation =
> the
> > reset=3D20 expression becomes true, then the overall evaluation of
> > the=3D20 property_spec is true, and is considered a vacuous success".
> >  Ben
> >  =3D20