Subject: Re: [sv-ac] RE: R44c - assume/check either, neither; must/should/could.
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Sep 12 2002 - 15:06:08 PDT
Hi Erich;
You write of three types of properties:
> 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.
>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?
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).
Thanks Erich.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Thu Sep 12 2002 - 15:09:08 PDT