RE: [sv-ac] vacuity

Hi John, Doron,

thank you for sending me your solution, I will look at it carefully.

Best regards,
ed
 

> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com] 
> Sent: Thursday, March 30, 2006 9:40 PM
> To: Eduard.Cerny@synopsys.COM
> Cc: john.havlicek@freescale.com; dbustan@freescale.com; sv-ac@eda.org
> Subject: 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
>