detailed proposal for adding synchronous abort

All,

Below is a detailed proposal for the LRM changes needed in order to
include a synchronous abort. The idea is the same as in my previous
email on the subject. The changes/additions are as follows.

1. Change of the rewording as per Johan's suggestion.
2. Rename the asynchronous abort operator "async_abort" to match
"sync_abort" and leave the "abort" operator for backwards
compatibility (with the semantics of async_abort).
3. A full list of changes to the LRM (previous proposal included only
changes to the abort section, appendices A and B).

Best regards,
Dana.

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

6.2.1.5.1 async_abort and sync_abort
The async_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 async_abort accepts asynchronous abort
conditions as well.

Box 54—abort operators
FL_Property ::=
FL_Property sync_abort Boolean |
FL_Property async_abort Boolean |
FL_Property abort Boolean

The left operand of the abort operators is the FL Property to be aborted.
The right operand of the abort operators is the Boolean condition that
causes the abort to occur.

Restrictions
None.

Informal semantics

An abort/async_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, with respect to the base clock, starting from the
current cycle and ending with the last cycle before the first 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_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, with respect to the base clock, starting from the
current cycle and ending with the last cycle before the first cycle in
which the Boolean condition that is the right operand and the context
clock both hold does not contradict the FL Property that is the left
operand.

Note
The abort operator is identical to the async_abort operator. It is
currently maintained in the language for reasons of backward
compatibility.

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

Example

Using async_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) async_abort cancel)@clk; or
always ((req -> eventually! ack) async_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

Rename abort as async_abort and add abort as syntactic sugaring which
is equivalent to async_abort.

3.
Changes to the BNF:

Add the products
FL_Property sync_abort Boolean
and
FL_Property async_abort Boolean
to
FL_Property

4.
Change all remaining occurrences of "abort" as follows:
a. Table 1 - add the keywords async_abort and sync_abort
b. Table 2 - add to the "FL terminator operator" line the operators
async_abort, sync_abort. Change "FL terminator operator" to "FL
terminator operators" (make it plural).
c. Section 4.2.3.2.8 - Change the text to talk about "FL terminator
operators" rather than "FL termination operator".
[
Entire section should read as follows:
4.2.3.2.8 FL termination operators
For any flavor of PSL, the FL operators with the next highest
precedence are the FL termination operators, used to specify a
condition which will cause both current and future obligations to be
canceled:
abort/async_abort/sync_abort immediate termination of current and
future obligations
The FL termination operators are left-associative
]
d. Section 6.2.4.1, page 82 - change the examples to use async_abort
rather than abort. Remove the parenthesis around "asynchronous" in the
text following the examples.
e. Section 6.2.4.2, page 83 - replace "abort" by "async_abort" in
the example (twice)

========================================================
Received on Tue Jan 25 12:22:27 2005