I've tried to analyze the problem from the bottom.


Assertion features related to the procedural code:

a) clocking,
b) enabling condition,

c) triggering,
d) control flow,

e) data sampling,
f) evaluation


Procedural code features related to the assertions:

i) clocking
ii) control flow



Today state:

assertion:

a) clocking: explicite or inferred
     - from procedural code: under case-specific rules only,
     - from external sources: clocking blok

b) enabling condition: explicite or inferred
     - from procedural code: under case-specific rules only,
     - from external sources: clocking blok

c) triggering: no special triggerring notion
d) control flow: no direct relation to the control flow

e) data sampling: preponed region
f) evaluation: observed region


procedural code:

i) clocking: no explicite notion of the process clock



Problems with embedding assertions in procedural code:

1) inferrence from procedural code

     i) clocking: no explicite notion for the process clock

     for a general 'always' process, the process clock needs to be determined by seeking for timing-control statements burried in the process code, the timing-control statements needs to met certain conditions to constitute a
(synthesisable) process clock,

     this leads to the numerous case-specific rules when assertion infers clock from code,

     assertions face same problem here as synthesis tools,
     lack of explicite process clock notion is cumbersome even for code reading - you have to carefuly analyze whole process code to determine if there is any consistent clocking in it ...


Possible solution:

     general: the process shall have explicite clock notion in it's header
(syntax) and no other timing-control statements allowed inside it's body,

     this way the clock inferrence feature would be clearly denoted in code,

     SV already have a always_ff process construct which meets these requirements (other processes: always @* , always_comb, always_latch - have a clearly defined clocking too).

     Shall we have restrict clock inferrence only to processes with explicit clock notion ?
     Shall it be always_ff only ?
     Or shall we introduce a general syntax extension for 'always' to denote process clock (which would restrict any other timing-control in the process body in turn) ?


2) assertions unrelated to the procedural code

     a) clocking: explicite or inferred from external sources: clocking blok
     b) enabling condition: explicite or inferred from external sources:
clocking blok

     this makes the assertion completely unrelated to the procedural code (unless we came up with any triggering/control flow relation) - so why it shall remain within the process text ?

Possible solution:

     disallow explicite clock specification or inferrence from external source - when assertion is placed within procedural code,
     assertion would always infer clock from the process - preferably explicitly denoted, the process may refer external clock definition (clocking blok) - but all the code block shall respect to the same consistent clock specification.


3) assertion relation to the control flow

     c) triggering: no special triggerring notion
     d) control flow: no direct relation to the control flow

     once the assertion is placed within procedural code - it is expected to have a direct relation to the control flow, otherwise users become suspicious about that construct ...

     an assertion triggering notion shall be explained first:

         triggering assertion would issue a 'seed' for new assertion trace, but to start the trace a valid enabling condition and clocking must occur in the same time-step, but not necessarily in the same delta/region,

         starting assertion can be seen as creating and dispatching assertion process thread, but keep in mind that the assertion evaluates in observed region,
         from this point of view assertion would be similar to the non-blocking assignment: the control flow activate it ,but the action happen in later region

         the assertion does not start new trace without trigger,
         if there was no triggering and the clocking event occurs - it may sustain evaluation of already started traces only

     there are two possible ways to establish relation with the control flow:

3a) triggering assertion by control flow

     the control flow pass thru the assertion statement will issue the trigger,

     this way the control flow will replace:  b) enabling condition,

     the clocking will remain independent from the control-flow, so:
         - the assertion needs to have the clock defined,
         - there is no need to recurring control flow to the assertion statement only to sustain already started traces,

     from this point of view assertion statement will act as 'fork' ...

     this scheme would fit today inital/always assert model

3b) triggering & clocking assertion by control flow

     the control flow pass thru the assertion statement will issue the trigger and serve as the assertion clock,

     this way the control flow will replace: a) clocking, b) enabling condition,

     this scheme is more demanding for the procedural code construction:
         - the control flow have to recurre to the assertion statement to allow next evaluation step,

     on the other hand it would allow more flexible assertion clocking that would be comparable to the capabilities of PSL 'next_event' operators family.

still the open question is: how the assertion shall behave if multiple triggers occur within same time-step:

- new trigger shall invalidate previous one ? this would be resistant to glitches,
- new trigger shall initiate new 'seed' including immediate data context ?
this would be compatible with the assertion in for-loop model,


4) data sampling

     e) data sampling: preponed region

     this default shall not be changed, an immediate/constant sampling - required in some cases (i.e.: in loops) shall be denoted with appropriate syntax, preferably:
     - per signal, (this style was already proposed by Gordon recently)
or:
     - per signal reference: this would allow to refer same signal with preponed sampling and with immediate/constant sampling from the same assertion.

-- ErikSeligman - 09 May 2008