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

Hi Shalom,

Unfortunately 17.11.2 is not a definition: it says only that if there is
no match of antecedent then the property passes vacuously. It does not
state that it is the only type of the vacuity.

But even this vacuity statement is not completely clear. Consider the
following example:

a |=> b

Let a happen at time t, and not happen anymore. If b happens at time t +
1 - does the property pass vacuously at the time t + 1 (remember that a
does not happen at t + 1)? Let alone it is not defined (at least I could
not find it) what means that the property passes or fails at the ***
given *** moment.

As for 17.3.3, though it is stated explicitly, I think that there are
semantic problems with the cover statement definition  and we should
address them first.

Thanks,
Dmitry

-----Original Message-----
From: Bresticker, Shalom 
Sent: Wednesday, February 22, 2006 12:01 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: 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