Extensions Group A - Discussion and Resolution

Results of discussion on 9 Nov 04:

Extensions Group A
==================

Issues (7,40)

7. Clarify effect of default clock declarations:
Default clocks apply to directives that don't have a clock. Should they also apply to declarations that don't have a clock? In particular, to endpoint declarations, which may be used in contexts that don't have a clock? And for that matter, does it ever make sense to define a sequence without specifying the clock (or applying the local default clock)? By extension, wouldn't it also make sense to specify (or apply) a clock when declaring a multi-cycle property? [EM 11 Aug 04]

>> Need reformulation, investigation. [JM 11Oct04]
>> Clarification is necessary one way or the other. Related to item 32. [EM 11Oct04]

40. Clocking of endpoints, prev etc.
Currently, the formal semantics does not deal with clocking "inside" booleans, which is very strange. This means that the clocking operator does not touch anything inside (compound) booleans, thus

     endpoint e = { a;b;c }

     assert always e@(posedge clk);

disregards the @(posedge clk) altogether, and e is clocked with some "system clock", which is tool dependent. The same is true for eg. prev(). [JA 11Oct04]

Discussion
==========

Avigail proposed that we always use the clock context of the place where the endpoint is used - this implies that we must be able to infer a clock from the modeling layer (or pass in a clock parameter, or include the clock explicitly in the endpoint declaration)

Discussion about how unclocked endpoint uses are affected by the clock context - see issue 40 also

Resolution
==========

1. Default clock definitions apply only to directives with no top-level clock. (No change to the current LRM definition.)

2. An instance of an unclocked endpoint declaration will inherit the clock context that applies at the location of the endpoint instance.

3. Any occurrence of built-in function rose, fell, or prev will inherit the clock context that applies at the location of that occurrence.

4. For each built-in function that is sensitive to the clock context (prev, rose, fell [and also stable]), add an optional Boolean parameter representing a clock expression.
Received on Mon Nov 15 19:08:41 2004