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

But |=> is defined in terms of |->, at least for now...
ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Bresticker, Shalom
> Sent: Wednesday, February 22, 2006 5:01 AM
> 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
> 
>