Group A - first draft LRM changes

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

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

LRM Changes for Group A

1. Define "clock context" in the LRM body.

Clause 4.4.1, Clocked vs. unclocked evaluation
- add the following initial paragraphs (note that this is part of a general rewrite of 4.4.1; see below):

  "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 apply only to 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 explicitly or may be inherited implicitly
   from an enclosing construct or region. An explicitly specified clock context
   takes precedence over an inherited clock context."

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. Explain how clock contexts are defined explicitly or inherited from an immediately containing construct or region.

- in Clause 5.2.3, Built-in functions, add:
  "For a built-in function reference that specifies a clock parameter, the clock
    context is that given by the clock parameter. For a built-in function reference
    that does not specify a clock parameter, the clock context is that of the clock
    expression, property, sequence, declaration, or directive in which the built-in
    function reference is immediately contained."

- in Clause 5.3, Clock expression, add:
  "For any clock expression, the clock context is the base clock context."

- in Clause 6.1.2, Sequences, add:
  "For an unclocked sequence, the clock context is that of the property, sequence,
    declaration, or directive in which the unclocked sequence is immediately
    contained."

- in Clause 6.1.2.5, Clocked SERE, add:
  "For a clocked SERE, i.e., a braced SERE that is the left operand of the @
    operator, the clock context is given by the right operand of the @ operator."

- in Clause 6.1.3.2, Sequence instantiation, add:
  "For an unclocked sequence instance, the clock context is that of the property,
    sequence, declaration, or directive in which the unclocked sequence instance
    is immediately contained."

- in Clause 6.1.4.2, Endpoint instantiation, add:
  "For an unclocked endpoint instance, the clock context is that of the property,
    sequence, declaration, or directive in which the unclocked endpoint instance
    is immediately contained."

- in Clause 6.2.1, FL Properties, add:
  "For a given unclocked property, the clock context is that of the property, sequence,
    declaration, or directive in which the given property is immediately contained."

- in Clause 6.2.1.2, Clocked FL properties, add:
  "For a clocked FL property, i.e., one that is the left operand of the @
    operator, the clock context is given by the right operand of the @ operator."

- in Clause 6.2.4.2, Property instantiation, add:
  "For an unclocked property instance, the clock context is that of the property,
    sequence, declaration, or directive in which the unclocked property instance is
    immediately contained."

- in Clause 7.1, Verification directives, add:
  "For a directive, the clock context is given by the applicable default
    clock declaration, if any; otherwise the clock context is the base clock context."

If we do not want the modeling layer to define a clock context, we should also add the following:

- in Clause 8, Modeling layer, add:
  "For modeling layer code, no clock context is defined. Any reference to built-in
    function calls prev(), stable(), rose(), or fell() must therefore include an explicit
    clock parameter to specify the clock context."

If we want to allow the modeling layer to define a clock context, and therefore allow use of built-in functions within the modeling layer without explicitly passing a clock parameter to each one, then we should instead add the following:

- in Clause 8, Modeling layer, add:
  "For modeling layer code, the clock context is the base clock context."

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

- in Clause 6.1.2.5, Clocked SERE, change the informal semantics to read as follows:
  "For unclocked SERE A and Boolean CLK:
       A@CLK holds tightly on a given path iff CLK holds in the last cycle of the given path,
      and A holds tightly on the path obtained by extracting the from the given path exactly
      those cycles in which CLK holds, and any subordinate sequences of A hold tightly as
      specified by A on the corresponding sub-paths of the given path."

- in clause 6.2.1.2, Clocked FL properties, change the informal semantics to read as follows:
  "For unclocked FL property A and Boolean CLK:
       A@CLK holds on a given path iff A holds on the path obtained by extracting
       from the given path exactly those cycles in which CLK holds, and any subordinate
       properties of A hold as specified by A at the corresponding cycles of the given path."

[Note: I'm not happy with this yet, but this is the best I've been able to do so far.]

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

- in Clause 5.4, Default clock declaration, change the informal semantics (first two paragraphs) to say:
   "The clock context of a directive is defined by the applicable default clock declaration,
    if any; otherwise the clock context of the directive is the base clock context."

[Note that the clock context of a directive such as "assert (always a)@c" may be True, even though the directive's clock context is superceded, or hidden, by the clock context of the property that is at the top level of the directive - in this case, c.]

6. Clarify how outer clock contexts affect references to prev/rose/fell/stable differently depending upon where those function references appear.

[This is accomplished by the addition of the explanation in clause 5.2.3 above, together with the removal of the repeated paragraphs 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)

as a Boolean (not 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)

as 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)

]

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

The above includes part of a proposed general rewrite of section 4.4.1, the goal of which is to also explain more precisely what kinds of properties must give the same results in simulation and in formal verification. A current draft of the full section 4.4.1 is below. The issue of equivalence between simulation and formal verification is partly related to the definitions of rose and fell, which are addressed above, and partly related to Group M, clocking and sampling.

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 apply only to 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 explicitly or may be inherited implicitly from an enclosing construct or region. An explicitly specified clock context takes precedence over an inherited clock context.

A PSL property or sequence whose clock context is specified explicitly by a clock expression attached to the property or sequence (via the @ operator; see Clause ...) is a /clocked/ property or sequence, respectively; otherwise it is an /unclocked/ property or sequence. An unclocked property or sequence inherits its clock context from an enclosing construct or region.

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.

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

Some issues with this draft that 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. Need to ensure that it is clear that the clock context of a property/sequence in which an instance appears flows into the (virtual) *instance* of the referenced declaration, not into the referenced declaration itself (which can be referenced from many different clock contexts).
3. 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).
4. Need to detail the changes required to clarify the equivalences of prev/rose/fell/stable.
Received on Tue Dec 14 09:44:21 2004