IEEE 1850 Extensions: Group A - Third draft LRM changes

From: Erich Marschner <erichm@cadence.com>
Date: Sat Jan 08 2005 - 17:18:36 PST

Following is a third draft of the changes required for Group A.
(See http://www.eda.org/ieee-1850/Issues/Group-A.html.)

================================================================

Changes relative to the previous (second) version:

1. In the update to 4.4.1, changed "previous declaration" to "default clock declaration". The paragraph now reads

A clock context may be specified locally, or may be inherited from an enclosing construct, or may be specified by a default clock declaration. A locally specified clock context takes precedence over an inherited or default clock context.

2. In the update to 5.3, changed the sentence about a built-in function used at the top level of a clock expression to require that it specify the clock context True, if any clock parameter is specified:

If a built-in function call that appears at the top level of a clock expression includes includes a parameter to specify the clock context of the built-in function call, the value of that parameter must be equivalent to True.

3. Removed the issue regarding specification of the clock context of Verilog event expressions.

4. Added the requirement that calls to prev/stable/rose/fell in the modeling layer must explicitly specify the clock context, through the addition of the following paragraph in clause 8, modeling layer:

If a built-in function call appears in the modeling layer, and the function is one that has an optional clock parameter, then the built-in function call must include an explicit clock expression to provide a value for that parameter.

5. Elaborated the changes to sections 5.2.3.x (prev/stable/rose/fell) to explain the additional, optional clock parameter, to add a note regarding the equivalence between versions with and without the additional parameter(s), and to explain how stable/rose/fell can be expressed in terms of prev.

(All of these changes appear below in the full proposal; the above is just a summary of the deltas from the previous version.)

================================================================

Remaining issues with this draft:

1. The outstanding issue regarding endpoints and default clocks may result in changes that will have to be factored into the following proposal.

2. The following must be coordinated with the proposed changes to account for the initial values of prev() and related functions.

=============================================================

Detailed LRM Change Proposal

=============================================================
1. Define "clock context" in the LRM body. This also addresses the issue of what
properties will give the same results in event-based vs. cycle-based verification.
=============================================================

4.4.1 Clocked vs. unclocked evaluation

A PSL property, sequence, endpoint, or built-in function can be qualified by a /clock context/ which causes the property, sequence, endpoint, or built-in function to be evaluated only in states in which the clock context holds. A nested property, sequence, endpoint, or built-in function within a given property or sequence can have a different clock context than that of the parent property or sequence.

The /base clock context/ is True, i.e., the granularity of time as seen by the verification tool. Different verification tools may model time at different levels of granularity. For example, an event-driven simulation tool typically has a relatively fine-grained model of time, whereas a cycle-based simulation or formal verification tool typically has a more coarse-grained model of time.

A PSL property or sequence whose clock context is specified locally by a clock expression associated with the property or sequence (by the @ operator) is a /clocked/ property or sequence, respectively; otherwise it is an /unclocked/ property or sequence.

A PSL property, sequence, endpoint, or built-in function whose clock context is equivalent to True is an /asynchronous/ property, sequence, endpoint, or built-in function; otherwise it is a /synchronous/ property, sequence, endpoint, or built-in function, respectively.

A synchronous PSL property that contains no nested asynchronous properties, sequences, endpoints, or built-in functions shall give the same result in cycle-based and event-based verification tools, provided that there is a one-to-one, in-order correspondence between (a) the succession of event-based states in which a clock context of the property holds, and (b) the succession of cycle-based states in which the same clock context holds.

=====================================================================
2. Extend built-in functions prev, rose, fell, stable to include an optional clock parameter.
=====================================================================

- in Clause 5.2.3, Built-in functions, extend the syntax to allow

    Built_In_Function_Call ::=
        prev ( Any_Type [ , Number [ , Clock_Expression ] ] )
      | stable ( Any_Type [ , Clock_Expression ] )
      | rose ( Bit [ , Clock_Expression ] )
      | fell ( Bit [ , Clock_Expression ] )

====================================================================
3. Clarify how outer clock contexts affect references to prev/rose/fell/stable differently
depending upon where those built-in function calls appear.
====================================================================

[This is accomplished by the addition of the explanation in clause 5.3, described below, together with the removal of the repeated paragraphs in 5.2.3.x starting "The clock context ...", as described below. We also need to clarify the equivalences given in these sections, also described below. Note that text between vertical bars - e.g., |text| - should be in the font (courier?) used for code.]

- PREV

- in clause 5.2.3.1, prev(), add the following sentence to the end of the first paragraph:

If a third argument is specified and has the value |c|, the built-in function |prev()| gives the value of the expression in the |ith| previous cycle, with respect to clock context |c|.

- in clause 5.2.3.1, prev(), remove the second paragraph starting "The clock context ..."

- in clause 5.2.3.1, prev(), add the following note:

- STABLE

- in clause 5.2.3.3, stable(), change the first paragraph to read as follows:

The built-in function |stable()| takes an expression of any type as argument. With a single argument, |stable()| returns True if the argument's value is the same as it was at the previous cycle, with respect to the clock of its context; otherwise it returns False. If a second argument is specified and has the value |c|, the built-in function |stable()| returns True if the first argument's value is the same as it was at the previous cycle, with respect to clock context |c|; otherwise it returns False.

- in clause 5.2.3.3, stable(), remove the second paragraph starting "The clock context ..."

- in clause 5.2.3.3, stable(), change the third paragraph (beginning "The function |stable()| can be expressed ..." to:

- in clause 5.2.3.3, stable(), add the following note:

- ROSE

- in clause 5.2.3.4, rose(), change the first paragraph to read as follows:

The built-in function |rose()| takes a Bit expression as argument. With a single argument, |rose()| returns True if the argument's value is 1 at the current cycle and 0 at the previous cycle, with respect to the clock of its context; otherwise it returns False. If a second argument is specified and has the value |c|, the built-in function |rose()| returns True if the first argument's value is 1 at the current cycle and 0 at the previous cycle, with respect to clock context |c|, otherwise it returns False.

- in clause 5.2.3.4, rose(), remove the second paragraph starting "The clock context ..."

- in clause 5.2.3.4, rose(), change the third paragraph (beginning "The function |rose()| can be expressed ..." to:

- in clause 5.2.3.4, rose(), add the following note:

For any expression |e|, |rose(e)| is equivalent to |rose(e,True)|.

- FELL

- in clause 5.2.3.5, fell(), change the first paragraph to read as follows:

The built-in function |fell()| takes a Bit expression as argument. With a single argument, |fell()| returns True if the argument's value is 1 at the current cycle and 0 at the previous cycle, with respect to the clock of its context; otherwise it returns False. If a second argument is specified and has the value |c|, the built-in function |fell()| returns True if the first argument's value is 1 at the current cycle and 0 at the previous cycle, with respect to clock context |c|, otherwise it returns False.

- in Clause 5.2.3.5, fell(), remove the second paragraph starting "The clock context ..."

- in clause 5.2.3.5, fell(), change the third paragraph (beginning "The function |fell()| can be expressed ..." to:

- in clause 5.2.3.5, fell(), add the following note:

For any expression |e|, |fell(e)| is equivalent to |fell(e,True)|.

==================================================================
4. Explain how clock contexts are defined explicitly or inherited from an immediately
containing construct or region.
==================================================================

- in Clause 5.3, Clock expressions, change the informal semantics to read as follows:

A clock expression defines a clock context. A clock context determines the path on which an FL property, sequence, or Boolean is evaluated.

The path determined by a given clock context consists of the succession of states in which the clock context holds. The base clock context is True, which holds in every cycle and therefore represents the smallest granularity of time as seen by the verification tool.

A subordinate FL property, sequence, or Boolean may have an explicitly specified clock context that is different from that of the immediately enclosing construct.

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.

For a property or sequence, the clock context is
- specified by the @ operator, if present; otherwise
- inherited from the immediately enclosing property or sequence, if any; otherwise
- inherited from the property or sequence in which it (or an endpoint declared with it) is instantiated, if any; otherwise
- (for a top-level property or sequence) specified by the applicable default clock declaration, if any; otherwise
- True.

==========================================================
5. Update Default Clock Declaration semantics to link it to the discussion of
clock context.
==========================================================

- in Clause 5.4, Default clock declaration, change the intro sentence to say:
"A /default clock declaration/, shown in Box 23, specifies the clock context of the top-level property or sequence of any directive to which the default declaration applies."

- in Clause 5.4, Default clock declaration, delete the first two paragraphs of the informal semantics, which read as follows:

"If the outermost property of an assert, assume, or assume_guarantee directive has no explicit clock
expression, then the clock expression for that property is given by the applicable default clock declaration, if one
exists; otherwise the clock expression for the property is the expression True."

"Similarly, if the outermost sequence of a cover, restrict, or restrict_guarantee directive has no
explicit clock expression, then the clock expression for that sequence is determined by the applicable default
clock declaration, if one exists; otherwise the clock expression for the sequence is the expression True."

These are unnecessary now that 5.3 explains how clock contexts are defined and inherited.

===============================================================
6. Correct the informal semantics of '@' to allow for a nested subelement that has
a different clock context.
===============================================================

- in Clause 6, Temporal Layer, add the following:

In the following subclauses, the term "cycle" refers to states in which the clock context of the corresponding property, sequence, or Boolean holds, and the term "path" refers to a succession of zero or more such cycles.

- in Clause 6.1, Sequential expressions, add the following:

A sequential expression is evaluated on a path, which is defined by a clock context. Every sequential expression has an associated clock context that defines the path upon which the sequential expression is evaluated. For a given sequential expression, its clock context is either specified explicitly or inherited from the immediately enclosing construct, if any. For a sequential expression that is contained immediately within a directive, its clock context is specified by the applicable default clock directive, if any; otherwise its clock context is True.

- in Clause 6.2.1, FL properties, add the following just before the Note:

An FL property is evaluated on a path, which is defined by a clock context. Every FL property has an associated clock context that defines the path upon which the property is evaluated. For a given FL property, its clock context is either specified explicitly or inherited from the immediately enclosing construct, if any. For an FL property that is contained immediately within a directive, its clock context is specified by the applicable default clock directive, if any; otherwise its clock context is True.

- in Clause 6.2.1.2, Clocked FL Properties, change the intro text to include the following:

The @ operator specifies that the clock expression that is its right operand defines the clock context of its left operand.

...

Note: Default clock declarations (clause 5.4) and the optional clock parameters of certain built-in functions (clause 5.2.3) also specify clock contexts.

- in Clause 6.2.1.2, Clocked FL Properties, change the informal semantics to read as follows:

A property A@C1 is evaluated on a path P1 determined by clock context C1.

If A contains a subordinate endpoint or built-in function F with clock context C2, and evaluation of A involves evaluating F in some cycle N of P1, then F is evaluated on a path P2 determined by clock context C2 and ending at N.

If A contains a subordinate sequence S@C3, and evaluation of A involves evaluating S at some cycle M of P1, then S is evaluated on path P3 starting at M and determined by clock context C3.

If A contains a subordinate property B@C4, and evaluation of A involves evaluating B at some cycle M of P1, then B is evaluated on a path P4 starting at M and determined by clock context C4.

- in Clause 6.1.2.5, Clocked SERE, change the intro text to include the following:

The @ operator specifies that the clock expression that is its right operand defines the clock context of its left operand.

...

Note: Default clock declarations (clause 5.4) and the optional clock parameters of certain built-in functions (clause 5.2.3) also specify clock contexts.

- in Clause 6.1.2.5, Clocked SERE, change the informal semantics to read as follows:

A sequence R@C1 is evaluated on a path P1 determined by clock context C1.

If R contains a subordinate endpoint or built-in function F with clock context C2, and evaluation of R involves evaluating F in some cycle N of P1, then F is evaluated on a path P2 determined by clock context C2 and ending at N.

If R contains a subordinate sequence S@C3, and evaluation of R involves evaluating S at some cycle M of P1, then S is evaluated on path P3 starting at M and determined by clock context C3.

- in Clause 8, Modeling Layer, following paragraph 6 (which begins "In each flavor of the modeling layer, ..."), add the following separate paragraph:

This archive was generated by hypermail 2.1.8 : Sat Jan 08 2005 - 17:19:07 PST