Re: Proposal to restore synchronous abort semantics

Erich,
For the record, to create a synchronous reset, SVA uses the triggered
method of a sequence. Thus:
sequence qAbort;
   @ (posedge clk) (reset || cancel);
endsequence : qAbort
 
property p_abr;
    @ (posedge clk) disable iff (qAbort.triggered)
        a |-> ##[1:4] b;
endproperty : p_ab
 
I have no objection to using the "@" or "@clk" as you proposed in
your proposals for abort and the default clock issues.
Ben Cohen

On Sun, 9 Jan 2005 20:49:53 -0800, Erich Marschner <erichm@cadence.com> wrote:
>
> 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 Sun Jan 9 21:12:02 2005