Re: [sv-ac] #1381

Hi Manisha,

Kulshrestha, Manisha wrote:

>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.
>  
>
The non-vacuous attempt is an auxiliary definition which help defining 
non-vacuous
success of evaluation attempt. At the end of 17.13.6 it says:

"An evaluation attempt of a property succeeds non-vacuously iff the property
 evaluates to true and the evaluation attempt is non-vacuous."

There is no definition of a non-vacuous failure and I don't see any 
value in having one.
I think that whenever there is a failure, either the design or the 
property need to be changed,
and thus the non-vacuity of the failure does not have any meaning.


>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 determines that
>p1 holds vacuously. Also assume that at t+10 simulator determines 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 vacuously or
>non-vacuously.
>  
>

I agree that there is an overhead here, but I am not sure how to avoid 
it. Note, that
every definition that will terminate the evaluation on "non-vacuous" 
whenever the
other property succeed, need not only to use the satisfaction relation, 
but also to define
when a property is evaluated to true. This is not well-defined yet. I 
would like to avoid
putting that into the definition.

On the practical side, I think of non-vacuous success as a witness that 
the property can be
computed through it's end (a coverage goal). So I do see value in 
keeping the simulator running.


>3. Page3 section 17.3.5, I agree with Ed and Bassam that evaluation
>attempt should not be dependent on the enabling condition.
>  
>

I will change that

Doron