RE: [sv-ac] #1381

Hi Doron, 

My thinking is that vacuity is a precondition so it's only a one "step"
decision (where you "wait" for other) beyond that is the "costly" part
... So the vacuous def form does allow you to short-circuit in or.

Thx.
-Bassam.

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Thursday, May 11, 2006 3:36 PM
To: Bassam Tabbara
Cc: Eduard Cerny; Kulshrestha, Manisha; sv-ac@eda.org
Subject: 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