IEEE 1850 Extensions: Re: Group A - Third draft LRM changes

From: Cindy Eisner <EISNER@il.ibm.com>
Date: Sun Jan 09 2005 - 00:50:50 PST

erich,

i think there is a contradiction between these two text fragments:

and

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

if prev(e,3) is equivalent to prev(e,3,true) as dictated by the first text
fragment, then that seems to imply that prev(e,3)@clk is equivalent to
prev(e,3,true)@clk. however, that is not the intention, and furthermore is
contradicted by the second text fragment.

i think what is needed is to replace the first text fragment with something
saying that if the optional clock context parameter is not supplied, then
the clock context is determined according to the rules in section xyz.

and similarly for the other built-in functions with optional clock context
parameters.

regards,

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

"Erich Marschner" <erichm@cadence.com>@eda.org on 09/01/2005 03:18:36

Sent by: owner-ieee-1850-extensions@eda.org

To: <ieee-1850-extensions@eda.org>
cc:
Subject: Group A - Third draft LRM changes

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 : Sun Jan 09 2005 - 02:15:59 PST