Re: Proposal to address default clock declaration issue - with corrected example

erich,

>Comments?

i am opposed to an optional right-hand operand of the @ operator. i think
that it will be extremely hard to parse (visually), especially with nested
clock properties. i would be less opposed, however, to adding the ability
to clock with the default clock using "@ default". i am even more in favor
of leaving things as they are now. i'm not really fond of the idea of
defining something as a default on the one hand, but on the other hand
requiring explicit syntax that says "use the default here".

i would also note that without any change at all, a user can get a similar
effect by defining a signal called, for instance, "my_clock" in the
modeling layer, then clocking with it wherever she so desires -
declarations as well as directives.

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 10/01/2005 04:44:47

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

To: <ieee-1850-extensions@eda.org>
cc:
Subject: Proposal to address default clock declaration issue - with
       corrected example

Proposal to address default clock declaration issue
=======================================

In the last Extensions SC meeting, I took an action item to discuss with
Steve Bailey a possible modification to the default clock declaration
semantics that would address his concerns. I did so, and the following is
a summary of the proposal that we discussed.

The central problem regarding the default clock declaration has been
whether it applies only to directives, or whether it also applies to
declarations. We've been arguing back and forth about this, even to the
point of considering the possibility of reclassifying an endpoint
declaration as a directive, so that default clock declarations would apply
to them.

I would like to suggest that the source of this issue is the fact that a
default clock declaration does two things at once, and it might be better
if we recognize and separate these two things. First, the default clock
declaration explicitly declares a default clock expression. Second, the
default clock declaration implicitly attaches that default clock expression
to any directive that has no top-level clock expression. There is no
problem with the first aspect of the default clock declaration; the issue
is that we cannot make the second aspect work in a way that will satisfy
everyone in all cases.

To address this problem, we propose a change that is non-backward
compatible, but that would grant much more flexibility and control to the
user. We propose to retain the default clock declaration syntax as it is,
with the existing meaning that it defines a default clock declaration that
is unique to the enclosing vunit. However, we propose to change the
association of the default clock with directives - or with declarations -
so that it is done explicitly, under user control.

Specifically, we propose to make the RHS argument of the @ operator
optional. If the RHS operand is not specified, then the default clock
expression defined by the applicable default clock directive is used as the
RHS operand.

This means that users would have to include at least the @ operator (as a
trailing, postfix-style operator) to indicate that a sequence or property
is clocked. This is a non-backward compatible change. However, this would
also allow the user to apply the default clock, and to do so quite easily,
in whatever context he/she wishes. It would also have the side benefit of
explicitly distinguishing clocked properties/sequences from unclocked
properties/sequences, whereas in PSL v1.1 an apparently unclocked property
or sequence in a directive can be affected by a default clock declaration
without any evidence of that in the directive itself.

Examples:

    default clock = rose(clk);
    ...
    // apply the default clock to an endpoint declaration
    endpoint e = {a;b;c}@;

    // apply the default clock to a nested property within
    // an unclocked property
    property p = always (a -> next (b until c)@ );

    // apply the default clock to a nested property within
    // an explicitly clocked property
    property p = always (a -> next (b until c)@ )@fell(clk);

    // apply the default clock explicitly to a directive
    cover {a; b; c; d}@;
    assert always ({a} |=> {b;c;d})@;

    // don't apply the default clock to directives implicitly
    cover {x; y; z}; // not clocked
    assert always ({x} |=> {y;z}); // not clocked

Comments?

Regards,

Erich
Received on Mon Jan 10 03:22:35 2005