Subject: Real Intent's Assertion Requirements with Justifications
From: Rajeev Ranjan (rajeev@realintent.com)
Date: Wed Jul 31 2002 - 00:17:38 PDT
Folks --
In the previous meeting it was suggested that the donors of the requirements
should also provide some justifications to facilitate understanding amongst the
committee members. Attached below is the modified version.
-Rajeev
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Rajeev K. Ranjan | Tel: (408) 982-5418
Director, R&D | Fax: (408) 982-5443
Real Intent |
3910 Freedom Circle, Suite 102A | rajeev@realintent.com
Santa Clara, CA 95054 | http://www.realintent.com
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
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.
J. A synchronous semantics will eliminate ambiguities about
interpreting assertions in presence of explicit delays present in
the design description. In addition, since scope of formal
analysis of assertions is most likely to be limited to zero-delay
models, adopting synchronous semantics eliminates the possible
different interpretation between an event-driven simulator and a
cycle-based simulator/formal analysis tool.
A2. The assertion format (syntax and semantics) must be compatible
with System Verilog.
J: A specification method which resides within HDL and whose
syntax and semantics is not completely consistent with that of HDL
will cause unnecessary learning curve and barrier to adoption.
A3. Must support the procedural method of specification. A procedural
assertion should have semantics equivalent to a non-blocking task.
J: A procedural method of specification enables us to leverage the
control flow within which it resides. Since the presence of
specification should not alter the design behavior, its semantics
should be non-blocking.
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.
J: See above.
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).
J: The interpretation of an assertion wrt assumption/guarantee
could change dynamically based on design context. It should be
possible to eliminate the user's burden of creating distinction
between assumptions and guarantees and leave it up to the analysis
tool to make appropriate distinctions.
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.
J: Usability.
B4. Must require a unique name reference to assertions.
J: This would provide a user with a convenient handle for various
control purposes.
C. Expressivity
C1. Must support a combinational expression on signals.
J. Bare minimum.
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.
J. Both types of temporal specifications are quite common in real
design environment.
C3. Must provide support for event sequence specification where a
Boolean expression is expected to occur (hold true) sometime in
the temporal window (see C2).
J. A common property: req implies ack must arrive within a
temporal window.
C4. Must provide support for event sequence specification where a
Boolean expression is expected to hold true throughout the given
temporal window.
J. A common input assumption: a req is held high through a
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.
J. Data bits should not toggle during read operation 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.
J. A state machine must make a transition within given temporal
window.
C7. The Boolean expression in B1-B6 should allow past and future
references of a signal.
J. Future references are quite common. In some circumstances, it's
more convenient to refer to past values.
D. Control Mechanisms
D1. Must support event based "acceptance"/"rejection" of the event
sequences in B3-B6.
J. Enables one to combine time based and event based temporal
window specifications.
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)
J. Provides for an easy specification method -- enabling one to
leverage the control flow of the design as an implied event
specification.
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).
J. This scheme would enable one to measure the effectiveness of
the stimuli being applied to DUT. In addition, formal analysis
could be used to establish if it's possible/impossible to meet
these coverage events. An impossibility would indicate a potential
design bug.
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.
J. This enables convenient nesting of event sequences for
assertion/coverage purposes.
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.
J. Having a clear-cut guideline about appropriate usage of
assertions for formal analysis would be immensely helpful for
users.
G. Refer to F above. In cases where there is ambiguity of semantics
interpretation by different verification technology, they should be
clearly identified.
J. Once again, identifying caveats where different verification
technologies could produce different results would be helpful to
the users.
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 00:23:51 PDT