Re: [sv-ac] #1381

Hi Manisha:

I don't follow your reasoning for (1).  The definition is of 
non-vacuity of attempt.  This is separate from success or failure.

I will repeat my comment that we should be careful about using 
the expected tool performance to change the definition.  Let's 
see what the competitive definition looks like for which the 
better tool performance is expected and see if anyone will use
it.  In the end, if the tool spends less time computing something
that no one finds useful, that is also a waste.

Best regards,

John H.


> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Thu, 11 May 2006 15:31:11 -0700
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] #1381
> Thread-Index: AcZ1QY91K8/OQpKqQhW/J4od6b35+gAA1tsg
> From: "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 11 May 2006 22:31:13.0396 (UTC) FILETIME=[9C1F3B40:01C6754A]
> X-Virus-Status: Clean
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id k4BMV7Nj012462
> Sender: owner-sv-ac@eda.org
> 
> Hi Doron,
> 
> For (1), since there is nothing like vacuous failure, the 'not P' can
> never result in vacuous success. Right ? 
> 
> If we have something like (not (not P)), and P has a vacuous success,
> (not P) will have failure as there is no concept of vacuous failure and
> so the overall property will pass non-vacuously.
> 
> For (2), I do not like the idea of putting overhead on the simulator. We
> need to come up with the definition such that it is not needed.
> 
> Thanks.
> Manisha
> 
> 
>  
> 
> -----Original Message-----
> From: Doron Bustan [mailto:dbustan@freescale.com] 
> Sent: Thursday, May 11, 2006 2:26 PM
> To: Kulshrestha, Manisha
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] #1381
> 
> Hi Manisha,
> 
> Kulshrestha, Manisha wrote:
> 
> >Hi Doron,
> >
> >Few comments/questions on the proposal:
> > 
> >1. So far LRM only had a concept of vacuous success but no vacuous 
> >failures. But in this proposal vacuous is not associated with success 
> >or failures. Does that mean that we now have vacuous success and 
> >vacuous failure ? If vacuous attempt is neither a success or failure, 
> >then should the action block be executed ? This question is more 
> >related to item (b) where you are defining not operator.
> >  
> >
> The non-vacuous attempt is an auxiliary definition which help defining
> non-vacuous success of evaluation attempt. At the end of 17.13.6 it
> says:
> 
> "An evaluation attempt of a property succeeds non-vacuously iff the
> property  evaluates to true and the evaluation attempt is non-vacuous."
> 
> There is no definition of a non-vacuous failure and I don't see any
> value in having one.
> I think that whenever there is a failure, either the design or the
> property need to be changed, and thus the non-vacuity of the failure
> does not have any meaning.
> 
> 
> >2. Regarding (c) p1 or p2, I have a problem with this. The simulator 
> >should not be forced to keep the evaluation attempt of a operand alive 
> >if the other operand has been determined to HOLD.
> >Say an attempt started at t then suppose at t+1 simulator determines 
> >that
> >p1 holds vacuously. Also assume that at t+10 simulator determines that 
> >P2 holds non-vacuously. So, eventhough the simulator has determined at 
> >time
> >t+1 that the property 'p1 or p2' HOLDS at time t, its been asked to 
> >t+keep
> >the evaluation of p2 alive to determine if 'p1 or p2' HOLDS vacuously 
> >or non-vacuously.
> >  
> >
> 
> I agree that there is an overhead here, but I am not sure how to avoid
> it. Note, that every definition that will terminate the evaluation on
> "non-vacuous" 
> whenever the
> other property succeed, need not only to use the satisfaction relation,
> but also to define when a property is evaluated to true. This is not
> well-defined yet. I would like to avoid putting that into the
> definition.
> 
> On the practical side, I think of non-vacuous success as a witness that
> the property can be computed through it's end (a coverage goal). So I do
> see value in keeping the simulator running.
> 
> 
> >3. Page3 section 17.3.5, I agree with Ed and Bassam that evaluation 
> >attempt should not be dependent on the enabling condition.
> >  
> >
> 
> I will change that
> 
> Doron
> 
>