RE: [sv-ac] Porposal assertion action control tasks

Hi Dimitry,

The answer to question (2) is 'no'. 

As per LRM: "The disable iff clause allows preemptive
resets to be specified. For an evaluation of the property_spec, there is
an evaluation of the underlying
property_expr. If prior to the completion of that evaluation the reset
expression becomes true, then the overall
evaluation of the property_spec is true."

So, in this case 'rst' will be checked before 'a' and the property will
have a disabled success. Since $assertdisableoff has been called for
this scope, the pass action 'action1' will not execute. 

I also agree that we need more clear definition of vacuous success.
Specially in the cases of multiple implication operators and also when
implication is used along with other operators (and, or etc.).

Thanks.
Manisha

-----Original Message-----
From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
Sent: Wednesday, February 22, 2006 1:46 AM
To: Kulshrestha, Manisha; sv-ac@eda.org
Subject: RE: [sv-ac] Porposal assertion action control tasks

Hi Manisha,

Here are my comments:

1) To define the action of $asservacuouson/of for assertions we need
first a clear definition of vacuous success of an assertion.

2) $assertdisabledon/off for assertions. Let's have the following
property:

assert property (disable iff(rst) a) action1 else action2;

Suppose both rst and a are high and $assertdisableoff has been issued.
Will action1 still take place?

3) cover statement. As I wrote in my previous mail, the definition of
cover statement itself needs a refinement. In my proposal the notions of
vacuous and disabled success for cover directives are irrelevant.

4) I definitely think that this is another errata item (if you are
talking about #805)

Thanks,
Dmitry


-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Kulshrestha, Manisha
Sent: Tuesday, February 21, 2006 7:25 PM
To: sv-ac@eda.org
Subject: RE: [sv-ac] Porposal assertion action control tasks

Hi All,

I am including a proposal for controlling action block execution. Please
send your feedback. Do we need another errata on this issue or this
proposal can be added to the errata on disable iff (which already has
another proposal).

Thanks.
Manisha