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

As far as I can see, the pass/fail decision is on a per-attempt basis.
They are reported separately, unlike the property like "globally a |=>
b" (not SVA!) where it is one single fail or pass.  

ed


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