Subject: RE: Assertions requirements from Real Intent
From: Erich Marschner (erichm@cadence.com)
Date: Wed Jul 31 2002 - 11:57:34 PDT
Wolfgang et al.,
I believe the question here was not why it should be possible to designate a property as an assumption - that is well understood, and in fact is explicitly supported in Sugar - but rather why it is important to do so *for simulation*.
Rajeev has argued that assumptions would be a source of constraints for directed-random simulation. I agree that interpreting properties to imply constraints on directed random simulation is worthwhile - but I would argue that tieing this to assumptions only is unnecessary.
In general, a simulator ought to be able to interpret any property - whether an assertion or an assumption - as indicating constraints for directed random simulation. In particular, assertions (or assumptions) about primary inputs of the block being simulated can easily be construed as such constraints. It is also possible to infer such constraints from assertions (or assumptions) about internal signals within a design, provided that the logic connecting those internal signals to primary inputs is taken into account. But there is no point in trying to verify an assertion about primary inputs in simulation, since such inputs are driven by the test bench itself, and we are verifying the design, not the test bench - so I would argue that there is no point in restricting the inference of input constraints for directed random simulation to consider only those properties labeled as assumptions.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Wolfgang.Ecker@Infineon.Com
| [mailto:Wolfgang.Ecker@Infineon.Com]
| Sent: Wednesday, July 31, 2002 3:06 AM
| To: EISNER@il.ibm.com; rajeev@realintent.com
| Cc: sv-ac@eda.org; assertion@eda.org
| Subject: AW: Assertions requirements from Real Intent
|
|
| 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 - 11:59:27 PDT