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

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] 
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 
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
>