RE: synchronous abort operator

andrew,

>For case C assuming PSL 1.1 async abort semantics, when does the
>assertion C fail? At time t4?

sorry for being picky, but i must rephrase that to "when do we know that
property C does not hold?" my point is not the recent assertion vs.
property discussion (although my answer incorporates that issue as well),
but rather that property C holds or does not for the whole trace, and thus
fails or does not for the whole trace.

the answer to my rephrased question is: we know that property C does not
hold at time t3 (because at time t3 p does not hold, and there is no
current or future cond2 - synchronous or asynchronous - that can "save
it").

BUT:

i think that your examples are missing the point of abort. for abort to be
interesting, the aborted property must take time to evaluate. then, if the
abort condition happens while we are still in the middle of evaluating the
property, it has the effect of "making the property true". in the examples
you give, the aborted property is simply "p", which is instantaneously
evaluated at each clock cycle.

i think better examples (on the same trace you sent) would be these:

always ((p -> next[3] !cond1) abort cond2)@(posedge clk)
(property F)
always ((p -> next[3] !cond1) sync_abort cond2)@(posedge clk)
(property G)

property F holds on the trace you sent, for the following reason: we need
to examine every assertion of p at a posedge of clk. there are three of
these times (unnamed in your trace). for each of these, we need to make
sure that cond1 is not asserted three cycles in the future. this is not
the case. therefore, the sub-property (p -> next[3] !cond1)@(posedge clk)
does not hold at either of these three times. however, in property F,
there is an asynchronous abort on condition cond2. the assertion of cond2
at time t2 in the trace "saves" each of three failures of the sub-property
(p -> next[3] !cond1)@(posedge clk), because in each case t2 occurs during
the time when the status of the sub-property is not yet determined.

property G does not hold on the trace you sent, because the abort is
synchronous. therefore, the assertion of cond2 at time t2 cannot "save"
the sub-properties.

regards,

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

"Seawright, Andrew" <Andrew_Seawright@mentorg.com>@eda.org on 12/01/2005
00:25:08

Sent by: owner-ieee-1850-extensions@eda.org

To: <dana.fisman@weizmann.ac.il>, "Erich Marschner" <erichm@cadence.com>
cc: <ieee-1850-extensions@eda.org>
Subject: RE: synchronous abort operator

The proposal looks okay to me. But to promote discussion I created
an example and waveforms to clarify the difference between how I
would expect the operators to differ assuming a posedge clock.
This example and waveforms illustrated in the attached GIF picture.
I'm assuming Verilog flavor in this example.

A: always(p)@(posedge clk); // fails at t3
B: always(p abort cond1)@(posedge clk); // holds
C: always(p abort cond2)@(posedge clk); // fails at t?
D: always(p sync_abort cond1)@(posedge clk); // holds
E: always(p sync_abort cond2)@(posedge clk); // fails at t3

If the abort condition pulses between clock edges, I would expect the
sync_abort operator to ignore this pulse.

For case C assuming PSL 1.1 async abort semantics, when does the
assertion C fail? At time t4?

I'm hoping that my waveform picture makes to the reflector...

Andrew

-----Original Message-----
From: Dana Fisman [mailto:dana.fisman@gmail.com]
Sent: Tuesday, January 11, 2005 12:54 PM
To: Erich Marschner
Cc: Seawright, Andrew; ieee-1850-extensions@eda.org
Subject: Re: synchronous abort operator

Erich, Andrew,

> I agree completely that there is a much greater need for synchronous
> abort than for asynchronous abort, and I would prefer to see this in
the language now.
> Nonetheless, I've agreed (reluctantly) to accept the status quo for
> now, in the interest of meeting our short-term goals.

I believe that it is very simple to add a sync_abort. That is, the
changes to the LRM are small and local. Below is a quick proposal I
wrote, which I believe its flaws are only in English and phrasing.
Perhaps if enough people review it early and agree, it can pass to the
LRM sub-committee by Tuesday.

Regards,
Dana.

========================================================
1.
Replace current section 6.2.1.5.1 about abort with the following section
about the two operators: abort and sync_abort.

6.2.1.5.1 abort and sync_abort
The abort and sync_abort operators, shown in Box 54, specify a condition
that removes any obligation for a given FL property to hold.
The sync_abort expects the abort condition to occur at a cycle when the
context clock holds. The abort accepts asynchronous abort conditions as
well.
Box 54-abort operators
The left operand of the abort/sync_abort operators is the FL Property to
be aborted. The right operand of the abort operator is the Boolean
condition that causes the abort to occur.
Restrictions
None.
FL_Property ::=
FL_Property abort Boolean |
FL_Property sync_abort Boolean

Informal semantics

An abort property holds in the current cycle of a given path iff:
- the FL Property that is the left operand holds, or - the series of
cycles starting from the current cycle and ending (not
inclusive) with the cycle in which the Boolean condition that is the
right operand holds does not contradict the FL Property that is the left
operand.

An sync_bort property holds in the current cycle of a given path iff:
- the FL Property that is the left operand holds, or - the series of
cycles starting from the current cycle and ending (not
inclusive) with the cycle in which the Boolean condition that is the
right operand holds and the context clock holds does not contradict the
FL Property that is the left operand.

Note
For unlocked properties aborting with abort or sync_abort is the same.

Example
Using abort to model an interrupt: "A request is always followed by an
acknowledge, unless a cancellation occurs."
always ((req -> eventually! ack) abort cancel);

Using abort to model an asynchronous interrupt: "A request is always
followed by an acknowledge, unless a cancellation occurs. The request
and ack signals are sampled at clock clk. The cancellation signal may
come asynchronously (not in a cycle of clk)."
always ((req -> eventually! ack) abort cancel)@clk; or always ((req ->
eventually! ack) abort cancel); when the default clock is clk

Using sync_abort to model a synchronous interrupt: "A request is always
followed by an acknowledge, unless a cancellation occurs. The request,
ack and cancellation signals are sampled at clock clk. A rise of the
cancellation signal when clk does not hold is ignored.
always ((req -> eventually! ack) sync_abort cancel)@clk; or always ((req
-> eventually! ack) sync_abort cancel); when the default clock is clk

2.
Change to the formal semantics:
Add the definition of |= and |=(c) for sync_abort as follows:

v |= \f sync_abort b iff either v |= f or \exists j<|v| s.t. v^j ||= b
and V^{0..j-1}\top^\omega |= f

v |=(c) \f sync_abort b iff either v |=(c) f or \exists j<|v| s.t. v^j
||= b&c and V^{0..j-1}\top^\omega |=(c) f

3.
Changes to the BNF:

Add the product
FL_Property sync_abort Boolean
to FL_Property

========================================================

On Tue, 11 Jan 2005 11:38:57 -0800, Erich Marschner <erichm@cadence.com>
wrote:
> Andrew,
>
> Speaking as chair of the Extensions SC: In the Extensions SC meeting
> today, we agreed that addition of a synchronous abort capability is
> worth pursuing, but that it would be deferred for now and will not
> make it into the June
> 2005 release. So the abort issue will be maintained in the Issues
> List for later discussion, and your comments will be noted in that
context.
>
> Speaking as myself (so that in the future, the above comments will not

> be misconstrued as reflecting my personal opinion): I agree completely

> that there is a much greater need for synchronous abort than for
> asynchronous abort, and I would prefer to see this in the language
> now. Nonetheless, I've agreed (reluctantly) to accept the status quo
> for now, in the interest of meeting our short-term goals.
>
> Regards,
>
> Erich
> ________________________________
> From: owner-ieee-1850-extensions@eda.org
> [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Seawright,
> Andrew
> Sent: Tuesday, January 11, 2005 2:27 PM
> To: ieee-1850-extensions@eda.org
> Subject: synchronous abort operator
>
> I would like to see a synchronous abort operator in PSL. If we must
> have an async abort operator semantics, then I would be in favor of
> another operator or way to denote a synchronous abort.
>
> For applications where the PSL assertions are clocked, most "disable"
> applications can be stated in synchronously. If the abort is
> synchronous, then the tools have more flexibility in terms of
> implementation and optimization.
>
> Andrew
>
>
>
Received on Wed Jan 12 01:47:50 2005