Subject: RE: [sv-ac] RE: R44c - assume/check either, neither; must/should/could.
From: Erich Marschner (erichm@cadence.com)
Date: Thu Sep 12 2002 - 16:14:59 PDT
Hi Adam,
| You write of three types of properties:
Well, three interpretations of properties - and I included the definition of "constraint" only to support the definition of "assumption".
| > Assertion: A statement that a given property is required
| to hold, and a
| >directive to verification tools to verify that it does hold.
|
| > Constraint: A condition (usually on the input signals)
| which limits the
| >set of behaviors to be considered.
|
| > Assumption: A statement that the design is constrained
| by the given
| >property, and a directive to verification tools to consider
| only paths on
| >which the given property holds.
| You excluded a fourth type:
|
| Coverage: A statement to report the occurrence of a
| given property.
It is a bit strange to talk about coverage of a *property*, as opposed to coverage of a particular *sequence*. (Sugar does support the latter, with the 'cover' directive.)
If you have a property of the form <antecedent> implies <consequent>, it is interesting to talk about coverage of the antecedent - i.e., whether the property has every been 'enabled' - but that usually amounts to sequence coverage.
| >No, I think simulation tools will also adhere to the
| meaning of both - but
| >in different ways. Simulation should check assertions, as
| FV tools do; but
| >there are at least two ways that simulation can consider
| only paths, or
| >scenarios, that conform to the given assumptions - by
| checking that the
| >assumptions hold (and ignoring any simulations for which
| they do not), or
| >by generating only simulation inputs that satisfy the assumptions.
|
| It would seem that you imply a connection between assumptions and
| assertions where now there is none. How would/should this be done?
| Why would this not be solved by including the name of the constraint
| in the antecedent of the property being verified?
But I think there is one. The designer specifies how the design should behave when it is operating properly within its environment. Assertions and assumptions are both involved in this specification. If there is a difference between the two at all, the difference is that assumptions express requirements on the environment of the design, whereas assertions represent requirements on the design itself. But because the boundary between the design and its environment is always moving outward (as today's design becomes a subcomponent of tomorrow's design), today's assumptions become tomorrow's assertions.
It is not sufficient to just "includ[e] the name of the constraint in the antecedent of the property being verified", because there may be multiple constraints, the conjunction of which must be satisfied for a given property to hold. Also, if there are multiple properties, you would have to repeat each constraint multiple times. This is one of the values of separating assertions and assumptions - so that the same (or different) combination(s) of assumptions can be used to verify each assertion. But the distinction is ephemeral - one run's assumption may be another run's assertion, and vice versa.
| It would seem to me that having an simulation check
| constraints in the
| module would be inviting the possibility of false firing. Now I am
| all for having these in the module, but one would need a method to
| disable these in simulation(s).
I don't quite follow this. If a design contains assumptions (i.e., input constraints), and simulation checks those assumptions during simulation, then the checks will fail only if the assumptions are not met. If, by "constraints", you mean restrictions that are not always applicable, then I agree that you don't want to check them in simulation all the time. But that's one of the reasons why you may want to specify such restrictions outside of the design - so they can be included in the verification run only when appropriate, and won't have to be removed, or turned off, during simulation.
Regards,
Erich
|
|
| Thanks Erich.
|
| Adam Krolnik
| Verification Mgr.
| LSI Logic Corp.
| Plano TX. 75074
|
-------------------------------------------
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
This archive was generated by hypermail 2b28 : Thu Sep 12 2002 - 16:16:18 PDT