Re: [sv-ac] #1381

Hi Ed and All:

I have been trying to follow the discussions, but not keeping
up too well.

I would like to see a coherent alternative inductive definition
for which the changes you are talking about for "or" and "not"
are incorporated.

What is wrong with having a tool switch to control how much 
effort the simulator puts in looking for non-vacuity?  If we 
use the tool performance as an excuse to break the definition,
then I'm afraid we will end up with a useless concept 

Regarding the attempts, I'm not sure we have done the right 
thing so far.

How does attempt counting work for immediate assertions?

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 14:00:38 -0700
> Thread-Topic: [sv-ac] #1381
> Thread-Index: AcZ0+HWrfPq94WVFRB+ELcrxclutewAN3PHgAAMvt2A=
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> X-OriginalArrivalTime: 11 May 2006 21:00:40.0182 (UTC) FILETIME=[F5AC9160:01C6753D]
> X-Virus-Status: Clean
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id k4BL0cNj011904
> Sender: owner-sv-ac@eda.org
> 
> Hello Doron et al,
> 
> A few comments regarding Manisha's comments:
> 
> 1. I think that the document defines only non-vacuous success by the
> sentence on pp2 just above Section 177.13.4, even though it defines
> non-vacuous attempt too, without qualifying what kind of outcome of the
> attempt takes place. I think this is useful. However, I agree with
> Manisha that the definition of the not operator is curious,  because to
> succeed, property_expr must have non-vacuous attempt and not
> property_expr must succeed. But that can happen only when property_expr
> fails.  Consequently, the failure must have been non-vacuous. How is
> that defined?
> 
> 2. I'd agree, because the user must realize that there is a choice in
> the property such that it can succeed if one of them has a vacuous
> success. Going beyond that can be unnecessarily costly.
> 
> 3. Not sure if it is clear what I meant - the condition is extracted
> from the procedural block, a syntactic extraction, into a concurrent
> property. hence vacuity etc. should apply the same way as if the user
> wrote the property outside the always block and copied the condition
> there manually.
> 
> I think that this also provides basis for extracting condition from,
> say, combinational always blocks for assertions embedded there, provided
> that the clock is explicitly specified in the assertion (which is what I
> said earlier in agreement with Dmitry.)
> 
> Best regards,
> ed
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> > Behalf Of Kulshrestha, Manisha
> > Sent: Thursday, May 11, 2006 4:39 PM
> > To: Doron Bustan; sv-ac@eda.org
> > Subject: RE: [sv-ac] #1381
> > 
> > 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.
> > 
> > 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 
> > determies that
> > p1 holds vacously. Also assume that at t+10 simulator 
> > determies 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 keep
> > the evaluation of p2 alive to determine if 'p1 or p2' HOLDS 
> > vacuosly or
> > non-vacuously.
> > 
> > 3. Page3 section 17.3.5, I agree with Ed and Bassam that evaluation
> > attempt should not be dependent on the enabling condition.
> > 
> > Thanks.
> > Manisha
> > 
> > 
>