Group A - second draft LRM changes

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

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

=============================================================
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 clock context may be specified locally, or may be inherited from an enclosing construct, or may be specified by a previous declaration. A locally specified clock context takes precedence over an inherited or previously specified clock context.

A PSL property or sequence whose clock context is specified locally by a clock expression associated with the property or sequence (via the @ operator; see Clause ...) 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 representing the previous explanation, as follows.]

- in Clause 5.2.3.1, prev(), remove the paragraph starting "The clock context ..."
- in Clause 5.2.3.3, stable(), remove the paragraph starting "The clock context ..."
- in Clause 5.2.3.4, rose(), remove the paragraph starting "The clock context ..."
- in Clause 5.2.3.5, fell(), remove the paragraph starting "The clock context ..."

[We also need to clarify the equivalences given in these sections, roughly as follows.]

[Define the following equivalences, probably in a Note, because these are consequences of other rules:

    prev(e,n,c) <==> prev(e,n) in the clock context c
    prev(e,1) <==> prev(e)

at the top level of a clock expression:
    stable(a) within a clock context c <==> (prev(a,1,True)==a)
    rose(a) within a clock context c <==> (prev(a,1,True)==0 && a==1)
    fell(a) within a clock context c <==> (prev(a,1,True)==1 && a==0)

not at the top level of a clock expression:
    stable(a) within a clock context c <==> (prev(a,1,c)==a)
    rose(a) within a clock context c <==> (prev(a,1,c)==0 && a==1)
    fell(a) within a clock context c <==> (prev(a,1,c)==1 && a==0)

]

[We also may want to require that any use of a built-in function in the modeling layer must include specification of the clock context via the optional clock parameter.]

==================================================================
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.

In particular, a built-in function call that appears at the top level of a clock expression has the clock context True, unless the clock parameter has been specified.

[Issue: this does not specify the clock context of Verilog event expressions that are used as clock expressions, so it does not specify on what path (posedge clk) would be evaluated. One could argue that this is appropriate, since posedge etc. are not defined as part of PSL. Alternatively, one might argue that we should define how posedge is interpreted in a cycle-based verification flow, since the Verilog LRM does not do so.]

==========================================================
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.

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

Some issues with this draft that may remain to be addressed:

1. Need to ensure that the definition of "unclocked ... instance" is clear - it is intended to mean an instance of a declaration that is unclocked.

2. May need to make it clear that clock expressions are by nature asynchronous, and that their asynchronicity does not affect the synchronousness of clocked properties (and therefore the expectation that, under appropriate circumstances, clocked properties will give the same result in both simulation and formal verification).

3. Need to detail the changes required to clarify the equivalences of prev/rose/fell/stable.
Received on Tue Dec 21 06:54:21 2004