RE: Proposal to restore synchronous abort semantics

Cindy, Johan, Dana,

I am clearly out-numbered in this discussion.

Although I was obviously party to the previous discussions, I did not agree with you at that time, nor do I agree now. I was convinced to drop the issue by you all, but I was asked in the last meeting (by Harry) to raise the issue again, for closure. I did so in the email I sent out last night, and I provided all the arguments I could for making a change. Clearly they have not convinced anyone.

I am surprised that none of you seem to see the inconsistency of this. Dana, Johan, you suggest adding an alternative, synchronous abort. So why don't we add an alternative, synchronous version of each operator, for symmetry? The answer is that the @ operator is defined to provide an easy way to clock properties, so it is not necessary to have both an asynchronous and a synchronous version of each operator. Why then should we apply that solution to abort? Beats me.

Cindy, I appreciate your point about the postfix operator being visually hard to parse. I would only point out that the lack of an explicit indicator that a directive is clocked is semantically hard to 'parse'. Yes, you are right that we accomplish the same thing through defining an explicit clock, but then we are no longer talking about the ease of use that the default clock declaration was intended to provide.

In any case, I retract my proposal, and I will agree not to bring the issue up again.

Regards,

Erich

| -----Original Message-----
| From: owner-ieee-1850-extensions@eda.org
| [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Cindy Eisner
| Sent: Monday, January 10, 2005 7:12 AM
| To: Johan Mårtensson
| Cc: ieee-1850-extensions@eda.org
| Subject: Re: Proposal to restore synchronous abort semantics
|
|
|
|
|
| erich,
|
| and just for the record, i completely agree with johan and dana.
|
| cindy.
|
| --------------------------------------------------------------------
| Cindy Eisner
| Formal Methods Group
| IBM Haifa Research Laboratory
| Haifa 31905, Israel
| Tel: +972-4-8296-266
| Fax: +972-4-8296-114
| e-mail: eisner@il.ibm.com
|
| Johan Mårtensson <johan.martensson@safelogic.se>@eda.org on 10/01/2005
| 12:44:44
|
| Sent by: owner-ieee-1850-extensions@eda.org
|
|
| To: ieee-1850-extensions@eda.org
| cc:
| Subject: Re: Proposal to restore synchronous abort semantics
|
|
| Hi Erich,
|
| I totally agree with Dana. You and I and Cindy had a long
| discussion on this issue before. I thought we came to the
| consensus that providing an abort operator for synchronous
| resets is desirable so we should plan to add that. This would
| provide all the capability asked for below. We should not
| however take away the current capability to express
| asynchronous reset because that would break backwards
| compatibility, and alignment with SVA, furthermore it is in
| many cases cumbersome to express asynchronous reset with a
| syncronous abort operator, your examples below
| notwithstanding. I think what you propose below is a
| regression to square one of that discussion.
|
| Best Regards, Johan M
|
|
|
| On Mon, Jan 10, 2005 at 10:46:59AM +0200, Dana Fisman wrote:
| > Erich,
| >
| > I understand that having a synchronous abort is desirable. I do not
| > understand why do you suggest to replace the existing
| (asynchronous)
| > abort. Why not have both? (i.e. leave the existing abort and add a
| > synchronous abort)?
| > Having both is surely the best way from the user point of view
| > (serving users who need asynchronous abort as well as users
| who need
| > synchronous abort as well as those who need both). It also
| solves the
| > alleged problem of alignment with SVA and the backwards
| compatibility
| > problem.
| >
| > Regards,
| > Dana.
| >
| >
| > 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 t
| > he 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
| > >
|
| --
| ------------------------------------------------------------
| Johan Martensson, PhD Office: +46 31 7451913
| R&D Mobile: +46 703749681
| Safelogic AB Fax: +46 31 7451939
| Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
| SE-411 33 Gothenburg, SWEDEN
| PGP key ID A8857A60
| www.safelogic.se
| ------------------------------------------------------------
|
|
|
|
|
|
Received on Mon Jan 10 05:59:14 2005