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

Hi Dmitry,

29.4.3 says twice that vacuity is defined in 17.11.2 and in 17.13. I
agree that it does not look like a definition, but it was apparently
intended to be one.

As for your example, as currently written, the LRM defines vacuity only
for |->, and your example uses |=>.

17.3.3 actually confuses the issue by saying that vacuity
rules apply to the 'implication operator', and |=> is also an
implication operator.

Bottom line: I agree that the LRM is ambiguous.

Shalom


> -----Original Message-----
> From: Korchemny, Dmitry
> Sent: Wednesday, February 22, 2006 12:16 PM
> 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