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
>>>
>>>
>>>      
>>>
>
>  
>