Re: [sv-ac] #1381

Bassam Tabbara wrote:

>Hi Ed/Manisha,
>
>For (2) below, yeah it bugs me now, I suggest to put (as I think I
>must've read it :)) "vacuous" for "nonvacuous" in the definition ...Do
>same for "and".
>
>That makes more sense, doesn't it ?
>
>Thx.
>-Bassam.
>  
>
changing the definition to"

An evaluation attempt of a property of the form
  property_expr1 or property_expr2 is vacuous iff either
  the underlying evaluation attempt of property_expr1 is vacuous
  or the underlying evaluation attempt of property_expr2 is vacuous

will not solve the overhead problem, because now if one
of the properties succeeds non-vacuously, the simulator
still need to check whether the other property is vacuous.

I think that a definition that will solve the problem 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 sure how to 
do that
without creating another overhead.


Doron