RE: Group A - second draft LRM changes

steve,

>2. The language is extended by adding a clocking block (there is no
>intention to base this on the SystemVerilog capability with the same
>name) which creates a region within which the clock expression applies
>to everything contained within, not just directives and it cannot be
>overridden (WYSIWYG):

two kinds of default clocks, one of which applies to declarations and one
of which does not, is an absolute recipe for confusion. i would rather
make a change to the current default clocks than introduce this extra
construct. (and just so i am not misunderstood: i am against making a
change, i'm just saying that if it comes down to choosing between the two,
making a change is better than this newest proposal.

>It would also be great if we could add a default abort where the
>semantics of the abort would include:
>
> - All assert and assume directives active when the abort expression
>becomes true will terminate and hold vacuously.
> - Any cover directive active when the abort expression becomes true
>will terminate without holding.
> - Any endpoint active when the abort expression becomes true will
>terminate without toggling true.
> - No directive or endpoint will start evaluation as long as the abort
>expression is true.

you seem to be looking for something like the asserton/assertoff capability
requested by ben cohen. this is related to, but probably separate from,
the abort operator. the reason is first that the abort operator already
has semantics, and they are not the semantics you describe above. first,
you can't today apply abort to a sere - thus not to an endpoint or to a
cover directive. second, even for properties, i don't think a default
abort gives you what you intended above.

for instance, consider the assertion

assert always (a -> next[3] b);

if an abort operator is applied to the above asserted property, we get:

assert (always (a -> next[3] b)) abort c;

thus, once the abort condition ("c") has been asserted once, the entire
property is "done". that is, another assertion of signal "a" will not
"turn it back on". you seem to be looking for something more like:

assert always ((a -> next[3] b) abort c);

where the abort is applied to the operand of always. to get what you want,
we'd have to define that a default abort applies to the operand of an
always statement. but what about properties without a top-level always?
for instance, what about the never operator?

much better, in my opinion, to define a totally new construct rather than
to redefine abort.

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

"Bailey, Stephen" <SBailey@model.com>@eda.org on 26/12/2004 17:57:56

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

To: Avigail Orni/Haifa/IBM@IBMIL, <ieee-1850-extensions@eda.org>
cc:
Subject: RE: Group A - second draft LRM changes

Hi Avigail,

(Tolerate the mis-application of existing PSL semantics in the 1st
paragraph that follows. They are there to present what I believe would
be the perspective of someone new to PSL based on their experiences with
other languages.)

If what you wanted with the assert directive was that a referenced
sequence be clocked by your default clock, then why did you apply a
default clock to the sequence (or perhaps more appropriately stated, why
did you reuse a sequence that was meant to be used in a different clock
context)? If the sequence is meant to be reusable, then the sequence
should've been left unclocked -- written prior to the default clock
specification -- or better yet it should've been parameterized by the
clock expression that would be applied in the context the sequence is
used. Otherwise, the sequence was never written to be reused in any
context. (It is accepted that it takes a bit more effort to write code
that is reusable. The amount of effort here is very small. Isn't it
worth it to increase the readability and maintainability of the PSL
code?)

I realize that 1.1 clearly states that default clocks apply at directive
level, but the reason I requested that we revisit the entire default
clock meaning is because of the hoops we are trying to jump through:

1. endpoints are being changed such that the default clock does not
apply to them. So, even though endpoints create something (are not just
macros), you must explicitly specify the clock or it will be unclocked.
Can anyone honestly say that this is not going to create confusion?

2. The following is not expected to create confusion?
> 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.

3. The discussion about adding clock context as a parameter to
built-ins is a further indication that it is confusing which clock
context applies and therefore users need to be able to specify it
explicitly for the built-ins.

The bottom line is that if the default clock specification is too
confusing to use, then it will be avoided and thus fail to satisfy the
requirements that gave rise to its existence. At a minimum, we are
already saying its utility is limited as people will need to write clock
expressions more frequently then they may have wished.

Let me make a proposal:

1. The current default clock specification continues to work as
specified in 1.1 with any clarifications in the LRM as needed. I still
don't like this, but I think it is necessary for backward compatibility.
Plus, it allows people who do like the existing semantics of default
clock to continue to use it.

2. The language is extended by adding a clocking block (there is no
intention to base this on the SystemVerilog capability with the same
name) which creates a region within which the clock expression applies
to everything contained within, not just directives and it cannot be
overridden (WYSIWYG):

block [<name>] [(parameter-list)] clock @clk is/=
  // Note parameter-list can contain the clock signal/expression

  ...

end;

It would also be great if we could add a default abort where the
semantics of the abort would include:

  - All assert and assume directives active when the abort expression
becomes true will terminate and hold vacuously.
  - Any cover directive active when the abort expression becomes true
will terminate without holding.
  - Any endpoint active when the abort expression becomes true will
terminate without toggling true.
  - No directive or endpoint will start evaluation as long as the abort
expression is true.

block [<name>] [(parameter-list)] clock @clk [abort rose(reset)[@clk]]
is/=
  // Note the parameter-list can also contain the reset/abort
signal/expr

  ...

end;

-Steve Bailey

> Steve,
>
> I guess WYSIWYG is somewhat in the eye of the beholder.
>
> If I see a declaration: sequence abc = { a; b; c } ;
>
> And, in a different vunit, see a directive: assert
> (always { abc } |=>
> {d})@clk1 ;
>
> What I see is a property clocked by clk1, and that's what I
> would expect to get. I would not expect 'abc' to be affected
> by some other clock that I don't see in the directive.
>
> I do see the validity of your viewpoint, but to me it is the
> less natural one. It probably depends on how we view named
> sequences -- whether they are just syntactic macros, or
> whether they carry some implicit contextual information, such
> as the clock that affects them.
>
> I do see a case for treating declarations and statements
> differently, if we intend to build libraries of (named)
> properties. We would like to make these properties as
> abstract and generic as possible, which means we would prefer
> not to specify the clock at the point of declaration.
>
> If we decide that the default clock at the point of
> declaration affects the named property when it is used, then
> we can't leave the declaration unclocked -- that would give
> it some fixed default clock wherever it is used (possibly the
> True clock). To avoid that, we would have to add a clock
> parameter to every named property and sequence in the
> library, and explicitly clock the declaration. So we may have
> saved typing in one place, but we've added it in another.
>
>
> Regards,
> Avigail
>
> _______________________________________________________
> Avigail Orni
> Verification and Testing Solutions Group IBM Haifa Research Laboratory
> Phone: 972-4-829-6396 email: ornia@il.ibm.com
>
> owner-ieee-1850-extensions@eda.org wrote on 22/12/2004 18:23:53:
>
> > 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 Mon Dec 27 00:56:02 2004