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 Tue Jan 11 12:55:07 2005