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

Hi Dmitry:

First, let me say I have not digested all the recent mail on this 
topic yet.

However, the discussion seems to be taking a turn that worries me.
I do not recall any effort in Section 17 to define what it means
for a property to pass or fail at a given point in a trace.  Instead,
we tried to discuss the idea of an evaluation attempt of a property
that begins at a given point and whose ultimate disposition may be
pass or fail (or, perhaps, pending at the end of a finite trace--
Annex E also defines neutral, strong, and weak variants of the finite 
trace semantics).

We did not attempt to define the point in the trace at which passing 
or failing of an attempt occurs, although in many simple examples it 
is intuitively clear what this point should be.  Rather, we tried to 
explain (without a careful structure of definitions and consequences
of them) whether an evaluation attempt that begins at a given point in 
a trace passes or fails.

So for your example, I would say that the evaluation attempt of 
"a |=> b" that begins at time t passes non-vacuously and the 
evaluation attempt that begins at time t+1 passes vacuously.

Shalom has pointed out that the notions of vacuous/non-vacuous
are not defined for "|=>".  I think that the intention was
that they apply to "|=>" as well, although it is not clear 
whether the test for non-vacuity of a passing evaluation attempt
of "R |=> P" should require a match only of R or of R followed by
some extra points in the trace (exactly which extra points should,
I think, depend on how the clocking event is or is not changing
across the |=> operator).  For most users, I expect that requiring 
R plus some extra points will be confusing, and we have, so far, left 
the interpretation of this detail to the tool implementation.

I think that a more careful definition of non-vacuity will need
to be given at some point.  In particular, the definition should
account for properties with nested implication operators.  For
example, in the case of 

   R |-> S |-> P

I think that the non-vacuity should require a match of "R ##0 S".

By the way, I have seen you lengthy comments on the semantics of "cover
property", and I intend to study them as soon as I can.

Best regards,

John H.


> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Wed, 22 Feb 2006 12:15:56 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Porposal assertion action control tasks
> Thread-Index: AcYr7RovyWojkVyBTtuINlTYhpj0RwAGu7FgAsDQ4OAAILZRAAACBJmwAABMNlA=
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 22 Feb 2006 10:15:57.0096 (UTC) FILETIME=[F8899280:01C63798]
> X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang)
> X-Virus-Status: Clean
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda.org id k1MAUx6T003680
> Sender: owner-sv-ac@eda.org
> 
> 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
>