RE: [sv-ac] vacuity

Hi Doron,

I agree with your proposal what the "top level" vacuity is concerned. If
I understood it correctly, it essentially says that the vacuity is
defined according to the top level binary operator; I am ignoring the
reset issue for the sake of simplicity. To be more accurate, if the
antecedent of the property in the implication normal form never matches,
and the property passes, it passes vacuously.

Nevertheless the user is often interested to get the partial vacuity
data as well. Consider the following example:

assert property ((a |-> b) and (c |-> d));

Suppose that a happens in the input word, but c never happens. According
to your definition the property passes non-vacuously, but the
information about the partial vacuity is also important. We need to
define some discrimination mechanism which will enable the exact
reporting. One option is to enumerate the implication operators inside a
property in a lexicographical order.

E.g., the reporting might be that the second implication executed
vacuously.

Therefore I am suggesting defining to kinds of vacuity - global vacuity
(= your definition) and partial vacuity (your definition with
appropriate modifications for or and and):

* For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$
iff
     $w,L \non P_1$ and $w,L\non P_2$.

 * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$
iff
     $w,L \non P_1$ and $w,L\non P_2$.

What do you think?

Dmitry

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Doron Bustan
Sent: Tuesday, April 11, 2006 1:00 AM
To: sv-ac@eda.org
Subject: [sv-ac] vacuity

I upload a new definition for vacuity.
The new definition differ from the old
one, at the "disable iff" operator.

Doron