RE: [sv-ac] #1381

Hi John,

I understand point (1) now. Do you think it will be useful to make it
clear in the proposal ? May be by providing example for 'not' operator ?

About (2), now that we have had some discussion and it looks like it is
not easy to comeup with a definition without a performance hit, I am
fine with the performance hit part. But I still have some concerns about
it because it is going to affect how simulation tools will report passes
(this does not affect formal tools though).
There are two issues with this:

1. We have had discussions in the past about changing the behaviour of
action block execution for vacuous passes. Almost everyone agreed that
pass action should not be executed on vacuous success. Now if we have a
pass action associated with (P1 or P2). If evaluation attempt starts at
t and P1 passes vacuously at t+1. Since we do not know the outcome of P2
yet, we can not decide if action block should get executed or not.
Suppose at time (t+5) P2 passes non-vacuously, then the action block
should get executed as overall property passed non-vacuously. But it is
too late to execute action block now. So, if we go by our current
proposal, it may not be possible to make changes in the current
semantics of action block execution.

2. There is also an issue with how simulators are going to show
assertion passes in the waveform. If simulator tool wants to show
vacuous/nonvacuous passes differently, if we take example given in (1),
by the time P2 passes non-vacuously, it will be too late to show
something in the waveform.

Thanks.
Manisha

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Friday, May 12, 2006 3:24 AM
To: Kulshrestha, Manisha
Cc: dbustan@freescale.com; sv-ac@eda.org
Subject: 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
> 
>