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

Dmitry,

'vacuous success' is defined in 17.11.2:

"If there is no match of the antecedent sequence_expr from a given start
point, then evaluation of the implication from that start point succeeds
vacuously and returns true."

This definition is sort of buried inside and not easy to find.

Note that it is defined only for |-> implication.
 
17.3.3 also says, "Vacuity rules are applied only when implication
operator is used."

Shalom


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
> Behalf Of Korchemny, Dmitry
> Sent: Wednesday, February 22, 2006 11: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