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