Re: [sv-ac] vacuity

Hi Ed:

You make a good point.  Doron and I have discussed this some, and
you will have seen Doron's mail.

Another approach is that we define that an attempt is "disabled"
if the disable condition occurs at or before the disposition (passing 
or failing) of the underlying property is determined.  Then we let the
categorization as "disabled" take first precedence, and only for 
a non-disabled attempt do we ask the question of whether it is
non-vacuous.  

I guess that this approach amounts to the same thing as what Doron 
wrote.

It would be good if our solution to the problem of defining "disabled"
and "vacuous/non-vacuous" attempts works seamlessly when nestable operators
"accept_on" and "reject_on" are added to the language.  I haven't
thought carefully enough about this to comment further at the moment.

Best regards,

John H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Thu, 30 Mar 2006 12:36:17 -0800
> Thread-Topic: [sv-ac] vacuity
> Thread-Index: AcZUOJBX3SFBQvDaQRa7npwCJpc4WwAAL4bg
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 30 Mar 2006 20:36:18.0314 (UTC) FILETIME=[98FBB6A0:01C65439]
> 
> Hello John,
> regarding
>  "b" in "disable iff (b) P", it does not affect "\non".
> But what if \non P holds only if you include the times when the disable
> condition is true and actually the property is disabled? Will you not
> get an optimistic result?=20
> 
> ed
> 
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=20
> > Behalf Of John Havlicek
> > Sent: Thursday, March 30, 2006 3:26 PM
> > To: dbustan@freescale.com
> > Cc: sv-ac@eda.org
> > Subject: Re: [sv-ac] vacuity
> >=20
> > All:
> >=20
> > Note that "\non" is a relation that defines when an evaluation
> > is non-vacuous.  "w,L \non P" does not imply "w,L |=3D P", so that=20
> > "\non" does not say anything about whether the evaluation results
> > in success or failure.
> >=20
> > The definition of "pass non-vacuously" would then be "w,L |=3D P"=20
> > and "w,L \non P".
> >=20
> > Regarding "b" in "disable iff (b) P", it does not affect "\non".
> >=20
> > Also, note that if we had followed_by, we would get
> >=20
> >    w,L \non R followed_by P
> >    iff  w,L \non not(R |-> not P)
> >    iff  w,L \non R |-> not P
> >    iff  w,L \non R |-> P
> >=20
> > Best regards,
> >=20
> > John H.
> >=20
> >=20
> > > Here is an attempt to define when an assertion pass non-vacuously.
> > > This proposal is also available at mentis (1381).
> > > This is not a proposal, it's a definition for review and discussion.
> > >=20
> > > There are a lot of vacuity definitions, I tried to have a=20
> > simple definition
> > > that generalizes the implication vacuity that is already=20
> > being used. The
> > > definition is on the structure of the property, on the=20
> > property level,=20
> > > meaning
> > > we have a new satisfaction relation. Let $\tight$ be the=20
> > tight satisfaction
> > > relation, $\models$ the satisfaction relation and $\non$ the
> > > non-vacuous  relation. An attempt of a property $P$ on a suffix $w$
> > > pass non vacuously iff $w,{}\models P$ and $w,{}\non P$.
> > >=20
> > > The definition of $\non$ is per attempt on a suffix $w$ of=20
> > a computation.
> > >=20
> > > Base: For every sequence $R$, property $P=3DR$, and=20
> > assignment $L$, we=20
> > > have that         =20
> > > $w,L\non P$.
> > >=20
> > > Induction:
> > >=20
> > >  * For $P =3D  (P_1)$ and assignment $L$, we have that=20
> > $w,L\non P$  iff
> > >      $w,L \non P_1$.
> > >=20
> > >  * For $P =3D R |-> P_1$ and assignment $L$, we have that=20
> > $w,L\non P$  iff
> > >      there exists $i \geq 0$, and an assignment $L_1$ such that
> > >      $w^{0..i}, {}, L_1 \tight R$ and $w^{i..}, L_1\non P_1$.
> > >=20
> > >  * For $P =3D P_1 and P_2$ and assignment $L$, we have that=20
> > $w,L\non P$  iff
> > >      $w,L \non P_1$ or $w,L\non P_2$.
> > >=20
> > >  * For $P =3D P_1 or P_2$ and assignment $L$, we have that=20
> > $w,L\non P$  iff
> > >      $w,L \non P_1$ or $w,L\non P_2$.
> > >=20
> > >  * For $P =3D not P_1$ and assignment $L$, we have that=20
> > $w,L\non P$  iff
> > >      $w,L \non P_1$.
> > >=20
> > >  * For $P =3D disable iff (b) P_1$ and assignment $L$, we have that=20
> > > $w,L\non P$  iff
> > >      $w,L \non P_1$.
> > >=20
> > >=20
> > >=20
> >=20