RE: Proposal to restore synchronous abort semantics

Hi All,

If it is desirable to support both synchronous and asynchronous aborts
in PSL (which the comments seemed to indicate that there was a consensus
that it is desirable) and

If it is problematic to specify a clock expression (@clk) with the abort
expression as that would make the abort expression a property and

It is silly (not to mention still not edge sensitive semantics) to "and"
the clock expression with the abort expression (rst && clk), then

Why not define an asynchronous abort operator (presumably the existing
abort operator) and a synchronous abort operator (let's call it sabort)?

sabort takes its clock context from the default clock or from an
optional, explicitly specified clock. Something like:

 ... sabort rst, rose(clk); // Explicit specification of clock

 ... sabort rst; // Implicit specification of clock.
Default clock is used

It would also be possible to do this without introducing a new operator
via generalization of the abort operator to take an optional clock
expression. If it isn't specified, then it defaults to TRUE
(asynchronous). The negative is that there would be no way to allow the
default clock to be used (again my problem with default not really being
the default and likely requiring additional typing the majority of the
time as the abort clock and directive clocks are likely the same most of
the time) and it is not quite as good at being self-documenting.

-Steve Bailey

> Proposal to restore synchronous abort semantics
> ======================================
>
> A few weeks ago, I raised an issue regarding the semantics of
> abort, which changed from PSL v1.01 to PSL v1.1, and in the
> process became strictly asynchronous in PSL v1.1, whereas in
> PSL v1.01 the abort condition had been sensitive to the clock
> context. I would like to propose an extension of the PSL
> v1.1 abort semantics that would restore the sensitivity of
> the abort condition to the clock context.
>
> Common applications of abort include the following:
>
> - asynchronous reset
> - synchronous reset
> - synchronous interrupt (in bus protocols, which are nearly
> always synchronous)
>
> The use of synthesis tools tend to encourage synchronous
> rather than asynchronous reset. Also, the increasing
> complexity of chips has led to increased use of synchronizing
> circuits for reset logic, so that the release of a reset is
> synchronized across the chip, and therefore all reset
> registers see the same first edge of the clock following release.
>
> A Google search on 'synchronous vs. asynchronous reset' turns
> up many references, most of which point to synchronous reset
> (and generally synchronous design) as being preferred. For
> example, there is a discussion of synchronous vs.
> asynchronous reset at the "Comp Help One" discussion forum,
> in entries under (Comp Arch FPGA/Async reset), at
> http://www.comphelpone.com/new-6338127-5158.html. See in
> particular the posts by Ray Andraka (Oct 21 2004) and by
> Peter Alfke (Oct 21, 2004). In the words of Mr. Andraka:
>
> "Generally speaking (asIC prototyping excepted...maybe), it
> is not advisable to use
> an async reset in the FPGA. The issue is that the release
> of reset is
> asynchronous to the clock, so you will get a situation
> where some flip-flops see
> the release on one clock cycle where others see the release
> on the next cycle when
> the reset is released close to the clock edge."
>
> This and other sources indicate that synchronous reset is
> more common than asynchronous reset, and that the trend is
> towards more synchronous reset. That being the case, we
> should ensure that PSL can support synchronous reset easily
> using the abort operator. I would also argue that
> synchronous reset should be supported in a manner consistent
> with the rest of the language, which uses the @ operator to
> define the clock context for synchronization.
>
> In the current (PSL v1.1) definition, abort is defined such
> that the RHS operand is not sensitive to the clock context,
> therefore regardless of whether there is a clock context
> present in the outer property, the abort operator is always
> asynchronous. A simple change to make the RHS operand
> sensitive to the clock context would allow abort to be used
> to express synchronous reset.
>
> The tradeoff for making this change is that expressing
> asynchronous abort might become more difficult. However, in
> the absence of a default clock declaration, expressing an
> asynchronous abort would be merely a matter of putting the
> abort clause outside the clocked property, rather than on the
> inside. That is, assuming that the abort condition is
> sensitive to the clock context,
>
> (1) always (P abort Q)@clk
>
> would model a synchronous reset by Q, whereas
>
> (2) always (P@clk) abort Q
>
> would model an asynchronous reset by Q. This is intuitively
> clear and completely consistent with the way in which the
> rest of the language is made synchronous or asynchronous.
>
> It has also been suggested that, if abort is nested within a
> property, then it becomes more difficult to make that abort
> asynchronous. The argument has been made that this will
> involve more text, because the inner abort will need to be
> protected with @True, and furthermore the @True will then
> apply to the LHS operand of the abort as well, so if the LHS
> operand needs to be clocked, then there is yet another clock
> expression required. For example, if we need to abort only
> the RHS of a suffix implication, and the suffix implication
> is clocked, and the abort models an asynchronous reset, it
> has been argued that we would have to write it as follows:
>
> (3) always ({a} |=> (({b}@clk abort reset)@true))@clk
>
> In fact, this can be written more simply, as
>
> (4) always ({a}@clk |=> ({b}@clk abort reset))
>
> so that once again the abort is outside the clock. It is
> true that, if we only want to abort the RHS operand of |=>,
> then we will have to write the suffix implication with clocks
> on both sides in order to be able to put the abort on the
> outside of the RHS clock. Nonetheless, I think that cost is
> a small price to pay for a consistent use model, and in any
> case the user may be just has happy to abort the whole suffix
> implication, in which case we are back to the simple solution:
>
> (5) always ({a} |=> {b})@clk abort reset
>
> For what it's worth, another solution for (4) is available
> now that we have clock context parameters on built-in functions:
>
> (6) always ({a} |=> {b} abort rose(reset,1,true))@clk
>
> Using the current semantics, an asynchronous abort is the
> default, and to make it synchronous one must literally 'and'
> in the clock with the abort condition. For example, the
> above cases would be expressed as follows in PSL v1.1:
>
> (1) always (P abort (Q&&clk))@clk
> or
> (1) always (P)@clk abort (Q&&clk)
>
> (2) always (P@clk) abort Q
> or
> (2) always (P abort Q)@clk
>
> (4) always ({a} |=> ({b} abort reset))@clk
>
> (5) always ({a} |=> {b})@clk abort (clk && reset)
>
> There are several reasons why the current definition is undesirable.
>
> The need to 'and' in the clock expression to get a
> synchronous abort is a special case mechanism that is not
> required elsewhere in the language. Also, the fact that the
> position of the abort operator (inside or outside the scope
> of the @ operator) does not matter is inconsistent with the
> rest of the language. Furthermore, the need to 'and' the
> clock to get a synchronous abort makes the property less
> reusable, because it forces a particular clock to be used
> explicitly. If a default clock applies to the outer
> property, the default clock might be changed without the user
> remembering to change the explicit abort clock. Note also
> that 'and'ing a clock only works if the clock is a Boolean;
> one cannot 'and' in a Verilog event expression such as
> (posedge clk). Finally, the current syntax is not clearly
> more efficient in any case except (4), and even there the
> improvement is minor, and even so, it may be more common to
> abort the whole suffix implication as in (5), for which the a
> lternative proposed here is simpler.
>
> Minimal LRM changes would be required to change the abort
> semantics back to being sensitive to the clock context.
>
> In Appendix B, the formal definition of clocked abort would
> have to change from
>
> v |=(c) phi abort b <==> either v |=(c) phi or there
> exists j < |v| s.t. v^j ||= b and v^(0..j-1)T^w |=(c) phi
>
> to
>
> v |=(c) phi abort b <==> either v |=(c) phi or there
> exists j < |v| s.t. v^j ||= (b && c) and v^(0..j-1)T^w |=(c) phi
>
> That is, the 'and'ing of the clock context would be done
> implicitly in the formal definition.
>
> In addition, the proposed informal semantics for 5.3, clock
> expressions, would have to change slightly. Specifically, in
> the definition of how the clock context is determined for a Boolean:
>
> For a Boolean, including an endpoint instance or built-in
> function call, the clock context is
> - (for a built-in function call only) specified by the
> optional clock parameter, if present; otherwise
> - inherited from the immediately enclosing Boolean
> expression or built-in function call, if any; otherwise
> - True, if it is the right operand of an abort operator; otherwise
> - True, if it appears immediately within a clock expression
> or in modeling layer code; otherwise
> - inherited from the immediately enclosing property or
> sequence, if any; otherwise
> - (for an endpoint instance only) inherited from the
> property or sequence in which it is instantiated, if any; otherwise
> - True.
>
> the line
>
> - True, if it is the right operand of an abort operator; otherwise
>
> must be deleted.
>
> No further changes would appear to be necessary. In
> particular, clause 6.2.1.5.1, abort, does not mention the
> fact that the abort condition in PSL v1.1 is insensitive to
> the clock context, and the example of an asynchronous abort
> given in that section does not involve a clock expression.
>
> Abort also occurs in other examples in the LRM.
>
> One occurrence is in 6.2.4.1, Property declaration, in which
> the following text appears:
>
> ==============================================================
> /Example/
>
> property ResultAfterN (boolean start; property result;
> const n; boolean stop) =
> always ((start -> next[n] (result)) @ (posedge clk)
> abort stop);
>
> This property could also be declared as follows:
>
> property ResultAfterN (boolean start, stop; property
> result; const n) =
> always ((start -> next[n] (result)) @ (posedge clk)
> abort stop);
>
> The two declarations have slightly different interfaces
> (i.e., different formal parameter orders), but they both
> declare the same property ResultAfterN. This property
> describes behavior in which a specified result (a
> property) occurs n cycles after an enabling condition
> (parameter start) occurs, with cycles defined by rising edges
> of signal clk, unless an (asynchronous) abort condition
> (parameter stop) occurs.
> ==============================================================
>
> This text is the same as it was in PSL v1.01, in which the
> abort condition was sensitive to the clock context, hence no
> change would be required. Note that in both cases, the abort
> appears outside the scope of @ operator, and the description
> characterizes the abort condition as asynchronous.
>
> Another occurrence is in 6.2.4.2, Property instantiation,
> which builds upon the example in 6.2.4.1. Here also there is
> no mention of the fact that in PSL v1.1, the abort condition
> is asynchronous regardless of the position of the abort
> operator w.r.t. the @ operator.
>
> One other objection has been voiced about the proposed
> change, namely, that this will affect alignment with SVA. I
> would argue that 'alignment' between PSL and SVA has never
> meant that one language should restrict itself to offer only
> the capabilities that the other language offers, and this
> case is no different. SVA is able to model asynchronous
> reset using the "disable iff" construct. Under the above
> proposal, PSL would still be able to model asynchronous reset
> also, using the abort operator under a clock context of True
> (often accomplished by just putting the abort operator at the
> end of the property). The fact that abort would also be able
> to model a synchronous reset should not be taken as a
> "misalignment" of PSL and SVA; instead it should be viewed as
> another example of where there is still room for both
> languages to grow by borrowing capabilities from the other.
>
> Regards,
>
> Erich
>
>
Received on Mon Jan 10 23:26:09 2005