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