erich,
good text! two comments:
1.
>A clock context may be specified locally, or may be inherited from an
enclosing construct, or may be specified by a >previous declaration.
i don't understand the phrase "a previous declaration". what is the
intention?
2.
>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.
i don't like the "unless the clock paramter has been specified". i think
that instead, we need a restriction such that clock expressions with clock
contexts other than true are not allowed.
>[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.]
the above suggestion solves this problem, i think.
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 21/12/2004 16:54:07
Sent by: owner-ieee-1850-extensions@eda.org
To: <ieee-1850-extensions@eda.org>
cc:
Subject: 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 Wed Dec 22 07:20:20 2004
This archive was generated by hypermail 2.1.8 : Wed Dec 22 2004 - 07:20:21 PST