RE: [sv-ac] #1381

Ed I am not thinking about cost now (although it got fixed as
side-effect). My reasoning is, in any choice, one branch is "vacuous"
and my overall determination of result is based on this so I should
leave this "marking" on the result ... 

Not to mention the sense of symmetry ...

Thx.
-Bassam.

-----Original Message-----
From: Eduard Cerny 
Sent: Thursday, May 11, 2006 2:15 PM
To: Bassam Tabbara; Eduard Cerny; Kulshrestha, Manisha; Doron Bustan;
sv-ac@eda.org
Subject: RE: [sv-ac] #1381

Hi,

I think that for "and" it should be as is. There, both must succeed and
so I think that at least one of them should be non-vacuous, it does not
cost any extra effort. 

ed

> -----Original Message-----
> From: Bassam Tabbara
> Sent: Thursday, May 11, 2006 5:12 PM
> To: Eduard Cerny; Kulshrestha, Manisha; Doron Bustan; sv-ac@eda.org
> Subject: RE: [sv-ac] #1381
> 
> Hi Ed/Manisha,
> 
> For (2) below, yeah it bugs me now, I suggest to put (as I think I 
> must've read it :)) "vacuous" for "nonvacuous" in the definition ...Do

> same for "and".
> 
> That makes more sense, doesn't it ?
> 
> Thx.
> -Bassam.
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of 
> Eduard Cerny
> Sent: Thursday, May 11, 2006 2:01 PM
> To: Kulshrestha, Manisha; Doron Bustan; sv-ac@eda.org
> Subject: RE: [sv-ac] #1381
> 
> 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
> > 
> > 
> 
>