Proposal regarding endpoints

A Proposal Regarding Endpoints
==============================

A concern still remains regarding clocking of endpoints. It has been argued that an endpoint both declares a name and creates a process that monitors the design, therefore it seems to be similar to a directive (to which default clocks apply), and therefore the default clock should apply to endpoints.

This confusion may come from the fact that endpoints are declared. Eliminating endpoint declarations, and providing an alternative way to refer to the endpoint of a sequence, might eliminate the problem.

It appears that we only ever need to declare one endpoint, namely

    endpoint ended(sequence S) = {S};

Given this declaration, we can refer to the end of any sequence by invoking this one endpoint. I suggest that we consider providing a built-in function for that purpose, and eliminate the need for endpoint declarations.

Function 'ended' could be defined as follows:

Built_In_Function_Call ::=
  ...
  | ended '(' Sequence [',' Clock_Expression ] ')'

The optional clock expression could be provided as shown above, to be consistent with prev/stable/rose/fell. Alternatively it could be left off, since the Sequence itself could be clocked.

The semantics of ended(S), for any sequence S (named or otherwise), would be exactly those of the current endpoint declaration, with S evaluated using the clock context of the property/sequence in which ended(S) appears. The semantics of ended(S,clk) - or equivalently, ended(S@clk) - would be the same, but in this case the clock context of S would be clk. (Note that this is consistent with the rules for clock context inheritance that we have already agreed upon.)

Examples:

  sequence US = {a;b};
  sequence CS = {a;b}@c;

  {x; ended(US); y} == {x; t; y} where t=end of {a;b}
  {x; ended(CS); y} == {x; t; y} where t=end of {a;b}@c
  {x; ended(US,clk); y} == {x; t; y} where t=end of {a;b}clk
  {x; ended(CS,clk); y} == {x; t; y} where t=end of {{a;b}@c}@clk == {a;b}@c
  {x; ended(US); y}@z == {x; t; y}@z where t=end of {a;b}@z
  {x; ended(CS); y}@z == {x; t; y}@z where t=end of {{a;b}@c}@z == {a;b}@c
  {x; ended(US,clk); y}@z == {x; t; y}@z where t=end of {a;b}clk
  {x; ended(CS,clk); y}@z == {x; t; y}@z where t=end of {{a;b}@c}@clk == {a;b}@c

With this change, the LRM sections on endpoint declarations and instantiations (which are largely redundant with sequence declarations and instantiations) would no longer be required. We could therefore simplify the LRM by removing section 6.1.4 Named endpoints and its two subsections, on pages 53-55 (PSL v1.1). The addition of the above 'ended' function would require addition of a section 5.2.3.x, ended(), with probably no more than two paragraphs.

We could also add the 'ended' function and retain endpoint declarations, if necessary for backward compatibility. If so, I would suggest defining ended(s) in terms of an anonymous endpoint declaration and instantiation, to make it clear that ended() is simply a shorthand for an endpoint instantiation. But if backward compatibility is not critical, I would recommend considering the removal of endpoint declarations in order to remove the confusion over whether default clock declarations apply to them.

Specific changes:

1. Add built-in function 'ended'

Change the syntax in Box 20 to include an entry for 'ended', with a Sequence parameter:

Built_In_Function_Call ::=
  ...
  | ended '(' Sequence [',' Clock_Expression ] ')'

2. Add a reference to 'ended()' in the first sentence following the box, after 'fell()'.

3. Add a new section 5.2.3.6 ended(), just after 5.2.3.5 fell(), with the following text:

The built-in function |ended()| takes a sequence as an argument. With a single argument, |ended()| returns True in any cycle in which the sequence completes; otherwise it returns False. If the first argument is |s|, and a second argument |c| is specified, then it is equivalent to |ended(s@c)|.

Note: In the absence of an explicit clock context parameter, the clock context is determined by the context in which the built-in function appears, as defined by the rules for determination of the clock context of a Boolean (specifically, a built-in function), given in section 5.3, Clock expressions.

[The above can be edited to remove the optional clock parameter, if we agree to do so.]

4. Remove section 6.1.4 Named endpoints and its subsections.

5. Remove references to endpoints elsewhere:
 - remove endpoint from the keyword list
 - remove endpoint from first paragraph of 5.2 Expression forms
 - remove Endpoint_Instance from the grammar in Box 17 and from the paragraph following
 - remove section 5.2.4.1 Endpoints
 - removed Endpoint_Instance from the grammar in Box 22 and from the paragraph following
 - remove reference to endpoint in 7.2, Vunit item
 - remove reference to endpoints in 8, Modeling layer
 - remove references to Endpoint_Declaration or Endpoint_Instance in appendix A:
     - in PSL_Declaration
     - all of Endpoint_Declaration
     - in Clock_Expression
     - in HDL_or_PSL_Expression
     - all of Endpoint_Instance
 - remove references to endpoint (and declaration, instantiation) in the index
Received on Tue Jan 25 07:31:26 2005