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

Hi Cindy,

> 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".

To me, "@ default" makes no sense as it saves virtually nothing in
typing. You might as well eliminate default clock altogether.

Personally, I see nothing wrong with a trailing @. Except that it is
postfix, it is analogous to Verilog's prefix @ for process sensitivity.
No one seems to have trouble with Verilog. I joked to Erich privately
that someone would complain that it should be prefix. While your
dislike of the trailing @ does not mention the Verilog prefixed @, I
wonder if you find that easier to humanly parse? If so, then maybe that
would point to something to consider.

> 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".

If you recall, the reason we are having this discussion is because
"default" in PSL does not mean default. It only means "directive".
Therefore, I'm not in favor of defining something as default when it is
not.

> 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.

Sure. But is this what we want people to do? After all, no one *needs*
PSL to do ABV. They can do everything in the modeling layer -- in HDL
code.

If default clock is to be true to its name, it should define a default
clock for any context and not just for directives. Erich's proposal
provides a way to explicitly state when something is clocked by the
default clock via a single character. So, the benefits I see are:

1. Default clock is true to its name.
2. Can be used for declarations and directives.
    (Declarations can defer their clock context or lock it down.)
3. The cost to use is very low and it is very simple to use (single
character).
4. Improves self-documenting characteristics of PSL code in that it is
clear when a directive or a declaration is synchronous versus
asynchronous (or, in the case of declarations, clocking decisions are
deferred).

The only negative is a break in backward compatibility in that
directives would need to add the @ character to be clocked by default
clock. However, I think it would be possible to grandfather in existing
semantics at the cost of losing the self-documenting benefits for
directives.

-Steve Bailey

> 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 10:46:06 2005