Following is a fourth draft of the changes required for Group A.
(See http://www.eda.org/ieee-1850/Issues/Group-A.html.)
================================================================
Changes relative to the previous (third) version:
1. To avoid a contradiction pointed out by Cindy, changed proposed notes about equivalence in 5.2.3.x (prev, stable, rose, fell) to
"In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions."
(In fact, the rules given in 5.3 determine how the clock context is determined whether or not the explicit clock context parameter is specified, because they highest priority rule is that the clock context parameter, if present, determines the context. This note is intended to point the user to the rest of the explanation - how a built-in function's clock context is inherited or not from enclosing constructs - if the first and most obvious indicator of clock context is missing.)
2. Removed the inappropriate reference to a 'number' parameter in the definition of how stable() can be expressed in terms of prev(), pointed out by Sitvanit.
3. To state more clearly the requirement that clock expressions are evaluated at the finest granularity of time as seen by the tool, added the following statement to section 5.3, Clock expressions to the paragraph defining 'base clock context' as True, representing the finest granularity of time as seen by the tool:
"A clock expression itself must be evaluated on the path determined by the base clock context. "
Also, changed the restriction previously added to a note, since it is now implied by the above statement.
(The above changes were suggested by Sitvanit.)
In doing so, I also removed the qualifier "at the top level" in "appears at the top level of a clock expression", because I believe the requirement applies at all levels - e.g., if rose(s,1,c) where c!=True is not legal as a clock expression, then (rose(s,1,c) && enable) should also be illegal as a clock expression.
4. Corrected two occurrences of "includes includes" (pointed out by Sitvanit) to read simply "includes".
================================================================
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 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 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.
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:
In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions.
- 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:
The function |stable()| can be expressed in terms of the built-in function |prev()| as follows: For any expression |e| and any boolean |c|, |stable(e,c)| is equivalent to the Verilog or SystemVerilog expression |(prev(e,c) == e)|, and is equivalent to the VHDL expression |(prev(e,c) = e)|. The function |stable()| can be used anywhere a Boolean is required.
- in clause 5.2.3.3, stable(), add the following note:
In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions.
- 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:
The function |rose()| can be expressed in terms of the built-in function |prev()| as follows: For any expression |e| and any boolean |c|, |rose(e,c)| is equivalent to the Verilog or SystemVerilog expression |(prev(e,1,c) == e)|, and is equivalent to the VHDL expression |(prev(e,1,c) = e)|. The function |rose()| can be used anywhere a Boolean is required.
- in clause 5.2.3.4, rose(), add the following note:
In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions.
- 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:
The function |fell()| can be expressed in terms of the built-in function |prev()| as follows: For any expression |e| and any boolean |c|, |fell(e,c)| is equivalent to the Verilog or SystemVerilog expression |(prev(e,1,c) == e)|, and is equivalent to the VHDL expression |(prev(e,1,c) = e)|. The function |fell()| can be used anywhere a Boolean is required.
- in clause 5.2.3.5, fell(), add the following note:
In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions.
==================================================================
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 clock expression itself must be evaluated on the path determined by the base clock context.
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.
Note: The fact that a clock expression must be evaluated on the path determined by the base clock context implies that, if a built-in function call appears in a clock expression and includes a parameter to specify the clock context of the built-in function call, then the value of that parameter must be equivalent to 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:
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.
Received on Sun Jan 9 09:51:18 2005
This archive was generated by hypermail 2.1.8 : Sun Jan 09 2005 - 09:51:20 PST