Re: [sv-ac] RE: P1800-2009 : Mantis 0002578 comments

Dmitry, Sorry, but I fail to understand your answer that addresses the a#-#
b rather than the
(not(a #-# b)).
Are you saying that if a==0, you get a "vacuous failure".  I don't believe
the LRM addressed the concept of "vacuous failure". Can we then clarify this
as :
6.15.8 Nonvacuous evaluations
d) An evaluation attempt of a property of the form not property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of
property_expr is nonvacuous, otherwise the evaluation will be vacuous
(vacuous fail).



On Mon, Feb 16, 2009 at 8:52 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

>  Hi Ben,
>
> According to this LRM definition, the failure may also be vacuous: this
> assertion fails in a "non-interesting" way – because a was false and not
> because b did not happen. Consider the following statement:
>
> cover property (@(posedge clk) start #-# cond);
>
> saying that we want to check cond when start happens. If start hasn't
> happened – there is no attempt, if it has and cond did not happen – we
> failed to cover it.
>
>
>
> Note that a #-# b is not (a |-> not b).
>
>
>
> Dmitry
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Saturday, February 14, 2009 7:05 AM
> *To:* sv-ac@eda.org
> *Cc:* Daniel.Mlynek@aldec.com.pl; Korchemny, Dmitry; Ajeetha Kumari;
> Srinivasan Venkataramanan
> *Subject:* P1800-2009 : Mantis 0002578 comments
>
>
>
> Dmitry
>
> The issue is the LRM
>
> 16.15.8 Nonvacuous evaluations
>
> d) An evaluation attempt of a property of the form *not *property_expr is
> nonvacuous if, and only if, the underlying evaluation attempt of
> property_expr is nonvacuous.
>
>
>
> *Question, when is it ever vacuous? *
>
>  a |-> b --> Vacuous success if a == 0. The "not" will negate it and
> hence:
>
> not (a |-> b) --> when"a == 0" is a FAILURE
>
>
>
> But logically, the intent here is as follows:
>
> not (a |-> b) should mean "never the case that (if *a==1, b==1)", *and if
> a==0, we don't care".  But this is not what "not (a |-> b)" says.  It
> says "never the case that (if *a==1, b==1)", *and if a==0, It's a ERROR".c
>
>
>
> Answers to Daniel Mlynek:
>
>   *<1. rule for or operator e)Results should be also vacuous if both prop1
> and prop2 are vacuous. *
>
> *I'm assuming than if prop1 is non-vacuous pass and prop2 is vacuous pass
> then result is nonvacuous> *
>
> *Ben: But either one or the other satisfy the requirement.  Doesn't that
> imply both? It's redundant. *
>
>
> *<4. Operator "not" also introduces ambiguity (for definition see below) -
> what should happen if property under not passes vacuously? We are geting a
> vacuous fail ?
> An evaluation attempt of a property of the form not property_expr is
> nonvacuous if, and only if, the underlying evaluation attempt of
> property_expr is nonvacuous.>*
>
> *Ben: Agree with the ambiguity.  The way the LRM stands, I don't see how
> the not operator on a property can produce a vacuous result.  In "**16.13.16
> Case", LRM brings the concept of true vacuous in "…**and the evaluation of
> the case property statement from that start point succeeds and returns true
> (vacuously)." **Thus, the not of a property that is vacuous, which is true
> vacuous, must be FALSE.   Consider the property expression:  a |-> b.  If
> "a==0", property expression is vacuous.  But "not(a |-> b)" sates never the
> case that if "a" then "b".  What happens if "a==0"? we should not really
> care, and the not of a vacuous property should  result in a vacuous result.
>  *
>
> *The  statement "**An evaluation attempt of a property of the form not
> property_expr is nonvacuous if, and only if, the underlying evaluation
> attempt of property_expr is nonvacuous." Seems to imply that result of a not
> of vacuous property is vacuous.  But vacuous is also considered as "true",
> thus not of true is false.  *
>
>
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.