RE: [sv-ac] #1381

But both must succeed, so there is no issue, no?
ed 

> -----Original Message-----
> From: Doron Bustan [mailto:dbustan@freescale.com] 
> Sent: Thursday, May 11, 2006 5:33 PM
> To: Bassam Tabbara
> Cc: Eduard Cerny; Kulshrestha, Manisha; sv-ac@eda.org
> Subject: Re: [sv-ac] #1381
> 
> I disagree
> 
> look for example on the non derived form of "if (b) p1 else p2;"
> which is "b |-> p1 and !b |-> p2".
> This is a reasonable property which will always have one
> of its operands succeeding non-vacuously.
> 
> Doron
> 
> Bassam Tabbara wrote:
> 
> >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
> >>>
> >>>
> >>>      
> >>>
> >
> >  
> >
> 
> 
>