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

Daniel, Point well taken.  However, 16.15.8 e) and 16.15.8 f) need to be
clarified.
Perhaps something without the "if and only if" as follows:
"An evaluation attempt of a property of the form property_expr1 or
property_expr2 is vacuous if the underlying evaluation attempt of one
property expression is vacuous and the other property expression is either
false or vacuous."

// By vacuous, we can have true or false vacuous.
// If any property expression inonvacuously true, than the OR is true.
Look someone want to express this in legalese term, I am open to it.
Ben

On Mon, Feb 16, 2009 at 11:55 PM, Daniel Mlynek
<Daniel.Mlynek@aldec.com.pl>wrote:

>  1)
> >Ben: But either one or the other satisfy the requirement.  Doesn't that
> imply both? It's redundant.
> The rule says:
> "An evaluation attempt of a property of the form property_expr1 or
> property_expr2 is vacuous if, and only if, either the underlying evaluation
> attempt of property_expr1 is vacuous and property_expr2 is false, or the
> underlying evaluation attempt of property_expr2 is vacuous. and
> property_expr1 is false."
>
> There is if and only if and && used in this definition - so strictly
> speaking it defines that
>
> property_expr1 == vacuous pass, property_expr2 = fail
> property_expr1 == fail, property_expr2 = vacuous pass
>
> the other combination according to this definition are no vacuous the
> others are:
> property_expr1 == pass pass, property_expr2 = vacuous pass
> property_expr1 == vacuous pass, property_expr2 = pass
> property_expr1 == pass, property_expr2 = pass
> property_expr1 == vacuous pass, property_expr2 = vacuous pass
> property_expr1 == fail, property_expr2 = pass
> property_expr1 == pass, property_expr2 = fail
> property_expr1 == fail, property_expr2 = fail
> .....
>
> at least one from above should results in vacuous pass:
> property_expr1 == vacuous pass, property_expr2 = vacuous pass
>
> 2)
> If IEEE wants to have smth like vacuous fail - it should be explicitly
> defined - ie should flase action block be triggered for vacuous fail etc...?
>
>
> DANiel
> ---------------------
>
> 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.
>
>

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