RE: Group A - second draft LRM changes

I agree with Cindy's proposal, but I think one point needs to be clarified:
what happens when a named construct declaration is not affected by any
relevant declaration clocks?

I think this should mean that the declaration of the named construct is
unclocked, and any instance of the named construct will be affected by the
clock at the point of instantiation.

This would allow us to create generic libraries of named properties, with
no declaration clock.
_______________________________________________________
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 04/01/2005 11:37:03:

>
>
>
>
> johan, steve,
>
> >> Yesterday, we talked about making endpoints a directive. Perhaps what
> >> we really need is two different beasts:
> >
> >Making endpoints a directive sounds very strange to me. What does that
> >mean?
>
> it sounds very strange to me as well. perhaps we can simplify as
follows:
>
> add the construct
>
> Clock_Declaration ::= declaration clock DEF_SYM Clock_Expression;
>
> the declaration clock (or any other name you want to call it) would be
the
> clock applied by default to all declarations, while the default clock
would
> be that applied by default to all directives. thus, both could be
> declared, or neither, or only one. if both are declared, they could be
the
> same clock or different clocks, of course.
>
> steve, does this address your concerns?
>
> 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
>
> Johan Alfredsson <johan.alfredsson@safelogic.se>@eda.org on 29/12/2004
> 20:00:39
>
> Sent by: owner-ieee-1850-extensions@eda.org
>
>
> To: "Bailey, Stephen" <SBailey@model.com>
> cc: ieee-1850-extensions@eda.org
> Subject: RE: Group A - second draft LRM changes
>
>
>
> Hi Steve,
>
> >> Moreover, your suggestion about writing things "prior
> >> to the default clock" does not change anything, as default
> >> clock affects _all_ directives in a vunit even if it is
> >> placed last in the vunit.
> >
> > Another inconsistency in PSL. In embedded PSL the default clock
applies
> > only to what follows until another default clock is specified. In
> > vunits, it applies to everything. (Again, I realize the LRM does not
> > cover embedded, but we can't ignore de facto standards.)
>
> This is a Mentor-specific thing and not industry standard. In principle I
> agree with you, and I actually tried to get this semantics into PSL a
> long time ago, but could not gain acceptance for that. Now I feel that it
> is too late to change anything regarding this.
>
> >> * What do you mean by changed? Endpoints has never been such
> >> that default
> >> clock applied to them.
> >
> > In our implementation, they did. This seems to be an error, but it is
> > one derived from the following.
>
> Yes, it is an error.
>
> >> * Endpoints _does not_ create anything per se -- how could
> >> they? consider
> >> parametrized endpoints.
> >
> > As I said yesterday, endpoints do create something. They create the
> > equivalent of a boolean-typed signal which can be referenced in other
> > sequences/properties/directives and in the modeling layer (HDL code).
> > If they didn't create anything, there wouldn't be a problem.
>
> Sorry, I could not attend the meeting yesterday. Regarding creation, I
> still don't think the declaration creates something. The usage of the
> declaration does, however. Otherwise, what would be created from
>
> endpoint my_rose(a) is { not a; a };
>
> ?
>
> However, when I write
>
> if e then
>
> in the modeling layer and there is an endpoint declaration called e,
> something will be created.
>
> If I understand you correctly, the main (only?) thing that bothers you is
> that you have to explicitly clock an endpoint to be able to use it with a
> certain clock in the modeling layer, and you don't like the clock to be a
> parameter to the endpoint. Am I right?
> If so, the whole thing is about convenience, and not functionality.
>
> I admit that having to write
>
> sequence s is { a; b[*]; c };
> endpoint e is { s };
> endpoint m_layer_e(boolean clk) is { s }@rose(clk);
>
> to be able to get the full generality of endpoints is a bit cumbersome.
> [That is also why I argued for using the HDL clock context for unclocked
> endpoints. This would amount to very few cases where you actually have
to
> write such an m_layer_e endpoint declaration with a clock parameter.]
>
> However, I prefer writing the above to your proposals below.
>
> > As we discussed yesterday, I believe there is a need to create an
> > endpoint and lock down its clock. The uses:
> >
> > - In the modeling layer for reactivity to sequences holding. (Could
> > be to take action on an error/success, as part of a complex checker
> > written in combined PSL and HDL, or it can be related to modifying
> > constraints for stimulus generation in the TB.)
>
> if m_layer_e(clk) then ...
>
> > - When referenced in another directive where the endpoint is meant to
> > be matched on a clock different from the one applied to the directive.
>
> default clock is rose(clk2);
> assert always e@rose(clk1) -> onehot(v);
>
> > I understand that there is a use for an unclocked endpoint
specification
> > where the clock that should be applied is "inherited" from the context
> > in which the endpoint is used. But, that is in *addition to* the need
> > for an endpoint that is locked down to a specific clock.
>
> default clock is rose(clk2);
> assert always e -> onehot(v);
>
> > Yesterday, we talked about making endpoints a directive. Perhaps what
> > we really need is two different beasts:
>
> Making endpoints a directive sounds very strange to me. What does that
> mean?
>
> > - An endpoint declaration: Does not create anything. Can only be
> > referenced in subsequent PSL sequences, properties, directives.
Default
> > clock specification does not apply to it (just like sequences and
> > properties).
>
> Given my statements above, this is what the endpoint declaration does,
> except that it also can be referenced in the modeling layer.
>
> > - An ended directive: Does create the boolean-typed signal which can
> > be referenced in the modeling layer. Default clock does apply to it.
> >
> > Perhaps a generalization of the existing cover directive could be
> > used as the ended directive? Instead of a boolean-typed signal
> > semantics, we would instead have an integer-typed signal initialized to
> > 0 and incremented whenever the sequence associated with the directive
> > holds.
> >
> > Or, if the boolean semantics are needed for formal or to make it easier
> > to use in a subsequent PSL context, cover provides a boolean-typed
> > signal semantics, but it also has an integer variable associated with
it
> > that is initialized to 0 and incremented by 1 in any cycle that the
> > cover holds. Then the modeling layer can reference the count via the
> > cover directive label (my_cover.count).
>
> This seems to be too simulation centric to go into PSL. You can always
> roll your own counters using the modeling layer.
>
> > In any case, there is a need for both a clocked endpoint (ended
> > directive) and an unclocked endpoint.
>
> I agree regarding the functionality, not at all regarding the directive
> etc. stuff. What is the big problem with what I showed above?
>
> > There is also a separate need to have a standard way to access the
cover
> > count of a cover directive -- at least in the modeling layer.
>
> This is a completely different issue, which should be discussed elsewhere
> if needed.
>
> Best regards,
>
> Johan Alfredsson Mobile: +46 706 39 12 58
> Product Manager Office: +46 31 745 19 00
> Safelogic Fax: +46 31 745 19 39
> Arvid Hedvalls Backe 4 johan.alfredsson@safelogic.se
> 411 33 Göteborg, Sweden www.safelogic.se
>
>
Received on Tue Jan 4 04:43:18 2005