RE: Group A - second draft LRM changes

All,

I have a problem with this discussion. The problem is that we are
forgetting why we are doing this to begin with: to make it easier for
the user to use PSL.

The trend of the discussion is to make it more difficult for users to
use PSL as they are required to do more typing and not less. Also, it
is more challenging mentally for the to understand the difference
between sequences, properties, endpoints and directives. The result is
not a WYSIWYG coding style. This is wrong and an indication that we
need to revisit the problem from square one.

If the purpose of a default clock specification is to eliminate the need
to specify @ <clk_expr> every time something is written, then why are we
forcing users to do so with sequences, endpoints, etc. This really
makes no sense at all to me and, I believe, makes it harder to learn and
understand PSL. It is almost like PSL needs to separate declarations
from statements. (I realize this doesn't apply to the declarative
nature of PSL, but if you want to add the syntactic sugaring to make it
easy for designers and verification engineers who know HDLs and C/C++,
then PSL needs to look more like those languages or it needs to be very
intuitive to use.) Sequences, properties and endpoints are declarations
and default clock specs and directives are statements. However, PSL has
no such lexical/semantic differentiation and it is unclear that such a
differentiation is desired.

If there is no differentiation, then the default clock spec must apply
to everything that occurs after it. Otherwise, it either fails to meet
its requirement (providing shorthand notation for users) or it makes the
language more complex to understand and use than desired.

Relatedly, there is an absolute need to have a default abort. I have
discussed this in the past with Erich and I realize there are precedence
issues that make a default abort difficult to manage. However, if I (as
a user) know that within the context of a module and/or vunit that there
is a single clock and a single reset, I should be able to specify the
defaults for both.

(BTW, adding a clocking expression to the builtins is OK as it adds
orthoganality. What I object to is that the default clock does not
apply to sequences, endpoints and properties, only directives and that
we don't have a default abort.)

Please, let's not lose sight of the end user here and the desire to make
PSL as easy to use and understand as possible.

-Steve Bailey
 
> 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 08:24:06 2004