Subject: Re: Assertions requirements from Real Intent
From: Rajeev Ranjan (rajeev@realintent.com)
Date: Tue Jul 30 2002 - 03:44:59 PDT
Hello Cindy --
My responses to your comments are embedded below.
- 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
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
----- Original Message -----
From: "Cindy Eisner" <EISNER@il.ibm.com>
To: <rajeev@realintent.com>
Cc: <sv-ac@server.eda.org>; <assertion@server.eda.org>
Sent: Monday, July 29, 2002 5:31 AM
Subject: 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?
>
An assumption in the context of System Verilog could serve the identical
purposes for both formal analysis and simulation verification methods.
As assumptions, they serve as environment constraints under which state
space search must be performed in formal analysis. In the same fashion one
can build simulation technology which produces pseudo-random vectors
respecting these assumptions which would be used to drive the design under
test.
These assumptions in the bigger context serve as objectives for interface
consistency verification. Once again, one can use formal analysis to verify
the interface consistency in the context of higher/bigger design entity or
alternatively can turn these assumptions as monitors which are tested while
the bigger design entity is being simulated under some testbench.
The procedural assertions within System Verilog could represent input
assumptions which are valid regardless of the state the design is in, e.g.,
always @(posedge clk)
assert(in1 ^ in2);
These assertions could also be used to EXPLICITY capture an input assumption
used for logic/fsm simplification by a designer -- as made famous by the
quote from Bob Bentley, Intel.
Finally, due to the concurrency of the hardware, an input assumption within
a procedural block affects the entire design -- and not just the procedure
its placed in. That means, within one state machine I can put the assumption
about a set of inputs even though these inputs are not affecting the state
machine directly. However, these assumptions could certainly affect the
behavior of another FSM in the design which is directly observing the same
set of inputs -- and thereby my whole design is being controlled by these
assumptions. This is in response to:
> 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.
Hope that answers your query. To elaborate on the requirement point -- I was
conveying that the language should not MANDATE the specific identification
of assumptions vs proof obligations by a user. A seamless process of
proof-obligation management by a tool should be permissible.
> >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?
>
Here is a pseudo-example.
always @(posedge clk)
case (state)
IDLE:
if (c1)
MY_ASSERT: assert than within 20 cycles event e1 occurs
READY:
if (c2)
accept(MY_ASSERT);
BUSY:
if (c3)
reject(MY_ASSERT);
ACK:
if (c4)
accept(MY_ASSERT);
In the above example, an assertion is triggered once the state machine is in
IDLE state and c1 is enabled. If we ignore the rest of the code then, the
assertion MY_ASSERT will pass if the event e1 occurs within 20 cycles,
otherwise it will fail. The rest of the code illustrates how this assertion
can be controlled -- made to PASS/FAIL -- based on various other events
occuring within the design. Notice that the "accept" and "reject" directives
are separated in the RTL from the actual assertion itself.
A common usage of this scheme that is used by our customers is -- MY_ASSERT
is specified WITHOUT any specific end time of the temporal window. The
assertion is terminated solely based on the events occuring in the design
elsewhere.
> >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?
>
Well there are many things that can fall in this category. We recognize the
fact that it will not be prudent to limit the expressivity of assertions to
only that set, which can be EFFICIENTLY verified by formal techniques. Some
examples of these would be "retriggerability" of assertions, very
deep/unbounded temporal specifications, multi-nested regular expressions
etc. It will be imperative to provide System Verilog users with a guideline
for writing assertions for efficient formal analysis.
> >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?
>
I am not sure if I would want to go to the extent of supporting delays in
formal analysis even though there is a well-defined semantics for it. I am
assuming that we are going to restrict formal analysis semantics to
zero-delay model only. And that itself could cause differences in the
results between an event-driven simulation and formal analysis. A few other
scenarios were discussed during DAS-1.0 discussions -- including how to
treat the re-firing of an assertion between two clock events (when a
sequential assertion is embedded in the combinational procedural code). My
point is that we should identify such scenarios and note any caveats if we
cannot reach an agreeement on identical semantics across all technologies.
> 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 : Tue Jul 30 2002 - 03:53:31 PDT