Subject: AW: Assertions requirements from Real Intent
From: Wolfgang.Ecker@Infineon.Com
Date: Wed Jul 31 2002 - 00:06:05 PDT
Hi Cindy,
I second the request, that an assertion should allow to identify
an assume/prove (as we say) or assume-guarantee-reasoning part.
Background is, that both, a formal tool and a simulator is used to
verify the code. To allow the formal to to consider both, the
assetions as well as its own properties, it must be able to
distinguish between the various aspects of the asserion.
Wolfgang Ecker
Verification Methodology Group
Infineon Technologies
-----Ursprüngliche Nachricht-----
Von: Cindy Eisner [mailto:EISNER@il.ibm.com]
Gesendet am: Montag, 29. Juli 2002 14:32
An: rajeev@realintent.com
Cc: sv-ac@eda.org; assertion@eda.org
Betreff: Re: Assertions requirements from Real Intent
rajeev,
below please find my comments regarding your proposed requirements.
>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).
i don't understand what assume would mean in the context of systemverilog:
an assumption in formal verification is used in place of environment
modeling - i.e., when you don't want to explicitly describe the
behavior of the input signals to the design, but rather want to use the
neighboring block's specification as an assumption on the behavior of
the inputs. however, once you are inside of procedural code as in
systemverilog, then presumably you have input behavior. therefore, it
seems there is nothing to assume. what am i missing?
>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)
i don't understand this. what does it mean to spread accept/reject
directives around the rtl, separately from the assertion? can you give
an example?
>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.
this is very interesting. we define a subset for simulation using the same
reasoning (but backwards). can you give an example of something that
would belong to this subset?
>G. Refer to F above. In cases where there is ambiguity of semantics
> interpretation by different verification technology, they should be
> clearly identified.
it seems to me that if we define the semantics well, then there should be
no ambiguity. can you clarify what you mean?
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
rajeev@realintent.com (Rajeev Ranjan)@eda.org on 25/07/2002 07:34:30
Sent by: owner-assertion@eda.org
To: assertion@eda.org
cc:
Subject: Assertions requirements from Real Intent
Hello all.
Attached herewith is the requirement for assertion specification from
Real Intent. Please feel free to send email for any clarification.
Regards.
-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.
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.
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 00:08:46 PDT