Subject: Re: Assertions requirements from Real Intent
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Aug 20 2002 - 08:44:00 PDT
Hi Erich:
I have just a couple of comments.
> Hi Wolfgang,
>
> I can't quite follow your reply.
>
> I agree that it is important to know whether a property has been =
> 'triggered', as well as whether it passes or fails (or remains =
> undecided at the end of simulation) once it has been triggered.
>
> However, I don't see the connection between assumptions and triggering =
> of a property. Almost by definition, a 'trigger' is expected to be a =
> condition that occurs sometimes but not always. In contrast, an =
> assumption is a condition that is expected to hold always. The two are =
> not the same, as far as I can see. =20
>
> The closest I can come to a sensible interpretation of your response is =
> to imagine that, in simulation, one might use unconstrained random =
> vector generation, and assertions would be considered to be 'triggered' =
> only if the random vectors met all the assumptions present. But a more =
> efficient way of doing this would be to apply the constraints to the =
> random vector generation process - i.e., to do constrained random =
> vector generation - so that only those vectors that meet constraints =
> are simulated. In this approach, assumptions are always true during =
> simulation, and therefore any assertions are always 'triggered', in a =
> sense.
The simulation testcase might be directed (e.g., a regression testcase) or
directed-random (e.g., from randomized testcase generator). Either way,
the particular assumption might not already be guaranteed to hold on the
testcase.
Also, depending on the nature of the assumption (eventuality, e.g.)
it may not be tractable to use it for constrained random simulation.
Regards,
J.H.
>
> In my view, a more interesting type of 'triggering' to be aware of is =
> that embedded in the property itself. Given a property such as=20
>
> assert always a -> next b;
>
> clearly the property will pass if a never occurs - so it is important =
> to note when/whether a occurs, thus 'triggering' (or enabling) the =
> property to pass or fail non-vacuously. But the occurrence of a is not =
> an assumption - i.e., we don't=20
>
> assume a=3D=3D1'b1;
>
> Instead, we expect a to occur (or not) at arbitrary times.
>
> Have I completely missed your point?
>
> 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=20
>
> | -----Original Message-----
> | From: Wolfgang.Ecker@infineon.com=20
> | [mailto:Wolfgang.Ecker@infineon.com]
> | Sent: Tuesday, August 20, 2002 4:03 AM
> | To: Erich Marschner; Wolfgang.Ecker@infineon.com; EISNER@il.ibm.com;
> | rajeev@realintent.com
> | Cc: sv-ac@eda.org; assertion@eda.org
> | Subject: AW: Assertions requirements from Real Intent
> | =20
> | =20
> | Hallo,
> | =20
> | We had several discussions about that topic here at=20
> | Infineon. Independent from the property checking aspect, we
> | think that assumptions should be visible also in Simulation.=20
> | Idea is, that an assumption is a trigger for a prove.
> | If a prove is triggered, it is not only important to know=20
> | whether it failed (error) or passed (coverage) but also
> | whether it is undecided at a specific simulation time or at=20
> | the end of simulation.
> | =20
> | Wolfgang
> | =20
> | =20
> | =20
> | -----Urspr=FCngliche Nachricht-----
> | Von: Erich Marschner [mailto:erichm@cadence.com]
> | Gesendet am: Mittwoch, 31. Juli 2002 20:58
> | An: Wolfgang.Ecker@Infineon.Com; EISNER@il.ibm.com;
> | rajeev@realintent.com
> | Cc: sv-ac@eda.org; assertion@eda.org
> | Betreff: RE: Assertions requirements from Real Intent
> | =20
> | Wolfgang et al.,
> | =20
> | I believe the question here was not why it should be=20
> | possible to designate a property as an assumption - that is=20
> | well understood, and in fact is explicitly supported in=20
> | Sugar - but rather why it is important to do so *for simulation*.
> | =20
> | Rajeev has argued that assumptions would be a source of=20
> | constraints for directed-random simulation. I agree that=20
> | interpreting properties to imply constraints on directed=20
> | random simulation is worthwhile - but I would argue that=20
> | tieing this to assumptions only is unnecessary. =20
> | =20
> | In general, a simulator ought to be able to interpret any
> | property - whether an assertion or an assumption - as=20
> | indicating constraints for directed random simulation. In=20
> | particular, assertions (or assumptions) about primary inputs=20
> | of the block being simulated can easily be construed as such=20
> | constraints. It is also possible to infer such constraints=20
> | from assertions (or assumptions) about internal signals=20
> | within a design, provided that the logic connecting those=20
> | internal signals to primary inputs is taken into account. =20
> | But there is no point in trying to verify an assertion about=20
> | primary inputs in simulation, since such inputs are driven=20
> | by the test bench itself, and we are verifying the design,=20
> | not the test bench - so I would argue that there is no point=20
> | in restricting the inference of input constraints for=20
> | directed random simulation to consider only those properties=20
> | labeled as assumptions.
> | =20
> | Regards,
> | =20
> | Erich
> | =20
> | -------------------------------------------
> | 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=20
> | =20
> | | -----Original Message-----
> | | From: Wolfgang.Ecker@Infineon.Com=20
> | | [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
> | | =20
> | | =20
> | | Hi Cindy,
> | | =20
> | | I second the request, that an assertion should allow to identify
> | | an assume/prove (as we say) or assume-guarantee-reasoning part.
> | | =20
> | | 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.
> | | =20
> | | Wolfgang Ecker
> | | =20
> | | Verification Methodology Group
> | | Infineon Technologies
> | | =20
> | | =20
> | | -----Urspr=FCngliche 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
> | | =20
> | | =20
> | | rajeev,
> | | =20
> | | below please find my comments regarding your proposed=20
> | requirements.
> | | =20
> | | >B2. The assertion scheme should allow seamless assume-guarantee
> | | > reasoning -- without the need of requiring a user to=20
> | explicity
> | | > specify the proof process (identifying an assumption vs=20
> | | a check).
> | | =20
> | | i don't understand what assume would mean in the context of=20
> | | systemverilog:
> | | an assumption in formal verification is used in place of=20
> | | environment
> | | modeling - i.e., when you don't want to explicitly=20
> | describe the
> | | behavior of the input signals to the design, but rather=20
> | | want to use the
> | | neighboring block's specification as an assumption on=20
> | | the behavior of
> | | the inputs. however, once you are inside of procedural=20
> | | code as in
> | | systemverilog, then presumably you have input behavior. =20
> | | therefore, it
> | | seems there is nothing to assume. what am i missing?
> | | =20
> | | >D2. Must support C1 where accept/reject directives are spread
> | | > around in the RTL (i.e. need not be tied to the=20
> | location of the
> | | > assertion itself)
> | | =20
> | | i don't understand this. what does it mean to spread=20
> | accept/reject
> | | directives around the rtl, separately from the=20
> | | assertion? can you give
> | | an example?
> | | =20
> | | >F. The assertion framework is being created for multiple
> | | > verification technologies (event-driven simulation,=20
> | cycle-based
> | | > simulation, formal analysis, semi-formal analysis,
> | | > emulation). Since the formal analysis complexity is=20
> | significantly
> | | > higher than other verification technologies, a subset=20
> | | suitable for
> | | > formal analysis should be clearly identified.
> | | =20
> | | this is very interesting. we define a subset for simulation=20
> | | using the same
> | | reasoning (but backwards). can you give an example of=20
> | | something that
> | | would belong to this subset?
> | | =20
> | | >G. Refer to F above. In cases where there is ambiguity=20
> | of semantics
> | | > interpretation by different verification technology,=20
> | | they should be
> | | > clearly identified.
> | | =20
> | | it seems to me that if we define the semantics well, then=20
> | | there should be
> | | no ambiguity. can you clarify what you mean?
> | | =20
> | | regards,
> | | =20
> | | cindy.
> | | =20
> | | Cindy Eisner
> | | Formal Methods Group Tel:=20
> | | +972-4-8296-266
> | | IBM Haifa Research Laboratory Fax: +972-4-8296-114
> | | Haifa 31905, Israel =20
> | e-mail:
> | | eisner@il.ibm.com
> | | =20
> | | =20
> | | rajeev@realintent.com (Rajeev Ranjan)@eda.org on=20
> | 25/07/2002 07:34:30
> | | =20
> | | Sent by: owner-assertion@eda.org
> | | =20
> | | =20
> | | To: assertion@eda.org
> | | cc:
> | | Subject: Assertions requirements from Real Intent
> | | =20
> | | =20
> | | =20
> | | Hello all.
> | | =20
> | | Attached herewith is the requirement for assertion=20
> | specification from
> | | Real Intent. Please feel free to send email for any =
> clarification.
> | | =20
> | | =20
> | | Regards.
> | | =20
> | | -Rajeev
> | | =20
> | | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
> | | 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
> | | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
> | | =20
> | | The following list outlines Real Intent's requirements=20
> | for assertion
> | | specification standard. A large portion of the=20
> | requirements are the
> | | outcome of our experience with the end users and issues=20
> | | encountered in
> | | the adoption of assertion driven verification.
> | | =20
> | | The requirements are divided in following categories:
> | | =20
> | | A. Fundamentals
> | | =20
> | | A1. The assertions and various supporting components of assertion
> | | driven verification methodology must have synchronous=20
> | semantics:
> | | the discrete evaluation time points are clearly=20
> | identified by one
> | | or more design clocks.
> | | =20
> | | A2. The assertion format (syntax and semantics) must be =
> compatible
> | | with System Verilog.
> | | =20
> | | A3. Must support the procedural method of specification.=20
> | A procedural
> | | assertion should have semantics equivalent to a=20
> | | non-blocking task.
> | | =20
> | | B. Ease of Use
> | | =20
> | | B1. The proliferation of assertion based methodology will=20
> | be enabled
> | | by its adoption of the designers. Designers would capture the
> | | design properties and the assumptions made there in=20
> | while writing
> | | the RTL. The specification method must not pose a significant
> | | learning barrier for the targeted users.
> | | =20
> | | 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=20
> | vs a check).
> | | =20
> | | B3. Must provide keyword based specification of some very =
> commonly
> | | occuring relationships -- mutual exclusiveness,=20
> | membership in a
> | | set, exclusion from a set, detection of signal transition.
> | | =20
> | | B4. Must require a unique name reference to assertions.
> | | =20
> | | =20
> | | C. Expressivity
> | | =20
> | | C1. Must support a combinational expression on signals.
> | | =20
> | | C2. Must provide support for both "time-based" (e.g.=20
> | between 5 and 10
> | | clocks) and "event-based" (between read_assert and=20
> | grant_assert
> | | events) temporal windows.
> | | =20
> | | C3. Must provide support for event sequence specification where a
> | | Boolean expression is expected to occur (hold true)=20
> | sometime in
> | | the temporal window (see B2).
> | | =20
> | | C4. Must provide support for event sequence specification where a
> | | Boolean expression is expected to hold true=20
> | throughout the given
> | | temporal window.
> | | =20
> | | C5. Must provide support for event sequence specification where a
> | | Boolean expression is expected to hold its value=20
> | (true or false)
> | | throughout the given temporal window.
> | | =20
> | | C6. Must provide support for event sequence specification where a
> | | Boolean expression is expected to change its value (true=20
> | | or false)
> | | sometime in the given temporal window.
> | | =20
> | | C7. The Boolean expression in B1-B6 should allow past and future
> | | references of a signal.
> | | =20
> | | D. Control Mechanisms
> | | =20
> | | D1. Must support event based "acceptance"/"rejection" of the =
> event
> | | sequences in B3-B6.
> | | =20
> | | D2. Must support C1 where accept/reject directives are spread
> | | around in the RTL (i.e. need not be tied to the=20
> | location of the
> | | assertion itself)
> | | =20
> | | =20
> | | E. Other Applications
> | | =20
> | | E1. Assertion scheme should provide a mechanism to=20
> | specify an event
> | | sequence completion as a coverage objective. The=20
> | expressivity of
> | | such a specification should be identical to that in=20
> | B. The format
> | | required for "assertion" and for "coverage" should be=20
> | identical
> | | (modulo a keyword differentiator).
> | | =20
> | | 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=20
> | collection,
> | | or c) triggering the detection of yet another event sequence
> | | completion.
> | | =20
> | | =20
> | | 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=20
> | significantly
> | | higher than other verification technologies, a subset=20
> | suitable for
> | | formal analysis should be clearly identified.
> | | =20
> | | G. Refer to F above. In cases where there is ambiguity of=20
> | semantics
> | | interpretation by different verification technology, they=20
> | | should be
> | | clearly identified.
> | | =20
> | | =20
> | | =20
> | =20
This archive was generated by hypermail 2b28 : Tue Aug 20 2002 - 08:46:32 PDT