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

Hi Dmitry:

The action blocks are intended to execute (at most) once 
per evaluation attempt of the property.

There is no formal definition of when the action blocks
execute.  This is a known issue, although I don't think
it is in mantis (yet).  Please go ahead and open a mantis
issue for this.

There is a similar issue of defining when a subroutine
appearing in a property executes.  My intuition is that
if we solve the subroutine problem, then we should be 
able to derive from it a solution to the action block
problem.

I still need to read Manisha's latest document before I 
can comment further.  In general, there can be distinct
evaluation attempts whose dispositions are different but
whose dispositions are "determined" at the same time.

Best regards,

John H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0
> Content-class: urn:content-classes:message
> Date: Wed, 22 Feb 2006 16:22:19 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] Porposal assertion action control tasks
> Thread-Index: AcY3sGxu3Kyun80CSR6ZwtfPkExbGQAAz5Fg
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: "Bresticker, Shalom" <shalom.bresticker@intel.com>, <sv-ac@eda.org>
> X-OriginalArrivalTime: 22 Feb 2006 14:22:20.0313 (UTC) FILETIME=[64057890:01C637BB]
> X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang)
> 
> Hi John,
> 
> In Section 17.13.1 it is written:
> 
> The assert statement is used to enforce a property as a checker. When
> the property for the assert statement is evaluated to be true, the pass
> statements of the action block are executed. Otherwise, the fail
> statements of the action block are executed.
> 
> Let's consider the simplest property:
> 
> assert property (@(posedge clk) a) $display("OK") else
> $display("Failed");
> 
> The intention here is apparently not to issue one summary message at the
> end of the simulation, but rather on each rising clock: E.g., if a is
> 11100 then the first three times "OK" is printed, and the last two
> "Failed" is. Therefore we need a definition of property success or
> failure at a *** given *** cycle.
> 
> I think that the formal definitions are very important since they assure
> the tool compatibility and are a central part of the language
> standardization.
> 
> E.g., if a is 111001, what will be reported at the last cycle "OK" or
> "Fail"? the property cannot evaluate to true if it once failed. On the
> other hand, I suspect that most tools will report "OK".
> 
> I wanted to open an errata item in Mantis about this, but I would like
> first to make sure that I am not completely wrong here.
> 
> As for the vacuity is concerned, my problem is when the vacuity is
> reported; since Manisha suggested turning on/off reports on vacuous
> success. In my example a |-> ##1 b at the time t a is high and at the
> time t + 1 b is high, therefore the success is not vacuous and this new
> directive should not have any effect. On the other hand, at the time t +
> 1 a was low, therefore the antecedent was false and we should report the
> vacuous success at this very time.
> 
> I am trying to say that the things are not that clear as they seem, and
> we should work on the definitions first. Only then we will know what run
> time control directives are missing and what their exact format should
> be.
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Wednesday, February 22, 2006 3:00 PM
> To: Korchemny, Dmitry
> Cc: Bresticker, Shalom; sv-ac@eda.org
> Subject: Re: [sv-ac] Porposal assertion action control tasks
> 
> Hi Dmitry:
> 
> First, let me say I have not digested all the recent mail on this=20
> 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=20
> trace semantics).
> 
> We did not attempt to define the point in the trace at which passing=20
> or failing of an attempt occurs, although in many simple examples it=20
> is intuitively clear what this point should be.  Rather, we tried to=20
> explain (without a careful structure of definitions and consequences
> of them) whether an evaluation attempt that begins at a given point in=20
> a trace passes or fails.
> 
> So for your example, I would say that the evaluation attempt of=20
> "a |=3D> b" that begins at time t passes non-vacuously and the=20
> 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 "|=3D>".  I think that the intention was
> that they apply to "|=3D>" as well, although it is not clear=20
> whether the test for non-vacuity of a passing evaluation attempt
> of "R |=3D> 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 |=3D> operator).  For most users, I expect that requiring=20
> R plus some extra points will be confusing, and we have, so far, left=20
> 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=20
> 
>    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:=20
> > X-MS-TNEF-Correlator:=20
> > Thread-Topic: [sv-ac] Porposal assertion action control tasks
> > Thread-Index:
> AcYr7RovyWojkVyBTtuINlTYhpj0RwAGu7FgAsDQ4OAAILZRAAACBJmwAABMNlA=3D
> > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > Cc: <sv-ac@eda.org>
> > X-OriginalArrivalTime: 22 Feb 2006 10:15:57.0096 (UTC)
> FILETIME=3D[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
> >=20
> > Hi Shalom,
> >=20
> > 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.
> >=20
> > But even this vacuity statement is not completely clear. Consider the
> > following example:
> >=20
> > a |=3D> b
> >=20
> > 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.
> >=20
> > 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.
> >=20
> > Thanks,
> > Dmitry
> >=20
> > -----Original Message-----
> > From: Bresticker, Shalom=20
> > 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
> >=20
> > Dmitry,
> >=20
> > 'vacuous success' is defined in 17.11.2:
> >=20
> > "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."
> >=20
> > This definition is sort of buried inside and not easy to find.
> >=20
> > Note that it is defined only for |-> implication.
> > =20
> > 17.3.3 also says, "Vacuity rules are applied only when implication
> > operator is used."
> >=20
> > Shalom
> >=20
> >=20
> > > -----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
> > >=20
> > > Hi Manisha,
> > >=20
> > > Here are my comments:
> > >=20
> > > 1) To define the action of $asservacuouson/of for assertions we
> > > need
> > > first a clear definition of vacuous success of an assertion.
> > >=20
> > > 2) $assertdisabledon/off for assertions. Let's have the
> > > following
> > > property:
> > >=20
> > > assert property (disable iff(rst) a) action1 else action2;
> > >=20
> > > Suppose both rst and a are high and $assertdisableoff has been
> > > issued.
> > > Will action1 still take place?
> > >=20
> > > 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.
> > >=20
> > > 4) I definitely think that this is another errata item (if you
> > > are
> > > talking about #805)
> > >=20
> > > Thanks,
> > > Dmitry
> > >=20
> > >=20
> > > -----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
> > >=20
> > > Hi All,
> > >=20
> > > 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).
> > >=20
> > > Thanks.
> > > Manisha
> >=20