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