Re: [sv-ac] #1381

Kulshrestha, Manisha wrote:

>Hi Doron,
>
>For (1), since there is nothing like vacuous failure, the 'not P' can
>never result in vacuous success. Right ? 
>
>If we have something like (not (not P)), and P has a vacuous success,
>(not P) will have failure as there is no concept of vacuous failure and
>so the overall property will pass non-vacuously.
>  
>

No, that is not true because the definition of "non-vacuous success" is 
not inductive
and is done only at the top level of the property. A trivial example is:
"not not a |-> b" which may succeed vacuously if "a" does not hold.
A non-trivial example "not a |-> not b |-> c" which succeed vacuously if 
"a"
holds  and "b" does not. In his case the property "b |->c" is vacuous thus
"not b |-> c" is vacuous, thus "a |-> not b |-> c" is vacuous and the whole
property is vacuous. Since the overall evaluation of the property is true,
we have a vacuous success.



>For (2), I do not like the idea of putting overhead on the simulator. We
>need to come up with the definition such that it is not needed.
>  
>


I think that a definition that you are looking for is of the form

An evaluation attempt of a property of the form
 property_expr1 or property_expr2 is non-vacuous iff there exists a prefix
 of the computation for which, either
 the underlying evaluation attempt of property_expr1 is non-vacuous
 in the prefix and  property_expr2 does not pass before the end of the 
prefix,
 or the underlying evaluation attempt of property_expr2 is non-vacuous
 in the prefix and property_expr1 does not pass before the end the prefix.

The problem is that we need to define what "non-vacuous in the prefix" and
"does not pass before the end of the prefix" are. I am not know how to 
do that
without creating another overhead.

Another solution is to say that every evaluation attempt of a properties 
of the forms
"p1 or p2", "p1 and p2" is non-vacuous. We will miss some information 
this way,
but for the common case of a single implication, it will still work.

Doron