RE: [sv-ac] #1381

Hi Doron,

For (1), since there is nothing like vacuous failure, the 'not P' can
never result in vacuous success. Right ? 

If we have something like (not (not P)), and P has a vacuous success,
(not P) will have failure as there is no concept of vacuous failure and
so the overall property will pass non-vacuously.

For (2), I do not like the idea of putting overhead on the simulator. We
need to come up with the definition such that it is not needed.

Thanks.
Manisha


 

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Thursday, May 11, 2006 2:26 PM
To: Kulshrestha, Manisha
Cc: sv-ac@eda.org
Subject: 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 
>t+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