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 Sun Jan 9 18:45:06 2005