Re: [sv-ac] #1381

From: Doron Bustan <dbustan_at_.....>
Date: Fri May 12 2006 - 15:48:08 PDT
Hi Manisha,

Kulshrestha, Manisha wrote:

>Hi John,
>
>I understand point (1) now. Do you think it will be useful to make it
>clear in the proposal ? May be by providing example for 'not' operator ?
>
>About (2), now that we have had some discussion and it looks like it is
>not easy to comeup with a definition without a performance hit, I am
>fine with the performance hit part. But I still have some concerns about
>it because it is going to affect how simulation tools will report passes
>(this does not affect formal tools though).
>There are two issues with this:
>
>1. We have had discussions in the past about changing the behavior of
>action block execution for vacuous passes. Almost everyone agreed that
>pass action should not be executed on vacuous success. Now if we have a
>pass action associated with (P1 or P2). If evaluation attempt starts at
>t and P1 passes vacuously at t+1. Since we do not know the outcome of P2
>yet, we can not decide if action block should get executed or not.
>Suppose at time (t+5) P2 passes non-vacuously, then the action block
>should get executed as overall property passed non-vacuously. But it is
>too late to execute action block now. So, if we go by our current
>proposal, it may not be possible to make changes in the current
>semantics of action block execution.
>  
>

The question is what is the goal of executing the action blocks. If the 
action blocks should
be executed after a "meaningful success of an assertion", then it make 
sense to execute them
at time t+5 more than it make sense to execute them on t+1.

So I think that from this point of view, the current definition is 
probably better than the alternatives
that I mentioned.

>2. There is also an issue with how simulators are going to show
>assertion passes in the waveform. If simulator tool wants to show
>vacuous/nonvacuous passes differently, if we take example given in (1),
>by the time P2 passes non-vacuously, it will be too late to show
>something in the waveform.
>  
>

I disagree,  since we are talking about properties, I think that their 
evaluation
status: fail/vacuous success/non-vacuous success should be marked at the 
beginning
of the property evaluation attempt.

But as far as I know there have not been a discussion on sva debug yet 
(and maybe
there should not be one) so it hard to consider that.

Doron
Received on Fri May 12 15:48:05 2006

This archive was generated by hypermail 2.1.8 : Fri May 12 2006 - 15:48:17 PDT