The following list outlines Real Intent's requirements for assertion
specification standard. A large portion of the requirements are the
outcome of our experience with the end users and issues encountered in
the adoption of assertion driven verification.

The requirements are divided in following categories:

A. Fundamentals 

A1. The assertions and various supporting components of assertion
    driven verification methodology must have synchronous semantics:
    the discrete evaluation time points are clearly identified by one
    or more design clocks.

A2. The assertion format (syntax and semantics) must be compatible
    with System Verilog.

A3. Must support the procedural method of specification. A procedural
    assertion should have semantics equivalent to a non-blocking task.

B. Ease of Use

B1. The proliferation of assertion based methodology will be enabled
    by its adoption of the designers. Designers would capture the
    design properties and the assumptions made there in while writing
    the RTL. The specification method must not pose a significant
    learning barrier for the targeted users.

B2. The assertion scheme should allow seamless assume-guarantee
    reasoning -- without the need of requiring a user to explicity
    specify the proof process (identifying an assumption vs a check). 

B3. Must provide keyword based specification of some very commonly
    occuring relationships -- mutual exclusiveness, membership in a
    set, exclusion from a set, detection of signal transition.

B4. Must require a unique name reference to assertions.


C. Expressivity

C1. Must support a combinational expression on signals.

C2. Must provide support for both "time-based" (e.g. between 5 and 10
    clocks) and "event-based" (between read_assert and grant_assert
    events) temporal windows.

C3. Must provide support for event sequence specification where a
    Boolean expression is expected to occur (hold true) sometime in
    the temporal window (see B2).

C4. Must provide support for event sequence specification where a
    Boolean expression is expected to hold true throughout the given
    temporal window.

C5. Must provide support for event sequence specification where a
    Boolean expression is expected to hold its value (true or false)
    throughout the given temporal window.

C6. Must provide support for event sequence specification where a
    Boolean expression is expected to change its value (true or false)
    sometime in the given temporal window.

C7. The Boolean expression in B1-B6 should allow past and future
    references of a signal.

D. Control Mechanisms

D1. Must support event based "acceptance"/"rejection" of the event
    sequences in B3-B6.

D2. Must support C1 where accept/reject directives are spread
    around in the RTL (i.e. need not be tied to the location of the
    assertion itself)


E. Other Applications

E1. Assertion scheme should provide a mechanism to specify an event
    sequence completion as a coverage objective. The expressivity of
    such a specification should be identical to that in B. The format
    required for "assertion" and for "coverage" should be identical
    (modulo a keyword differentiator).

E2. Assertion scheme should provide a mechanism to specify the
    completion of an event sequence as an enabling condition for 
    - a) starting an assertion, b) starting coverage data collection,
    or c) triggering the detection of yet another event sequence
    completion. 


F. The assertion framework is being created for multiple
   verification technologies (event-driven simulation, cycle-based
   simulation, formal analysis, semi-formal analysis,
   emulation). Since the formal analysis complexity is significantly
   higher than other verification technologies, a subset suitable for
   formal analysis should be clearly identified.

G. Refer to F above. In cases where there is ambiguity of semantics
   interpretation by different verification technology, they should be
   clearly identified.