Subject: Re: [sv-ac] RE: R44c - assume/check either, neither; must/should/could.
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Sep 13 2002 - 08:14:18 PDT
Hi Erich;
Okay, I understand your point now...
>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.
1. Not all assumptions will be necessary for each assertion.
2. There may be many assumptions necessary for each assertion.
3. A property may be used as an assumption for another property.
So you suggest that assumptions may need to be separate from the design.
But the very real problem is that separate assumptions may not be
correct. You may not be able to prove an assumption you make due to
the design size [being too large.]
Thus I expect to see assumptions placed in the RTL. A tool could choose
to use all assumptions in proving an assertion, or choose to use
a subset (via specification.) But a simulation should check assertions
and assumptions the same - so that you don't have to duplicate
the intent as an assumption and a property textually.
>"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.
Yes!
If you want to have a 'constraint' placed in the RTL code so that you
don't need another container (file), I don't mind - I like this.
One just needs to be able to disable (simulation of) this constraint.
In summary:
#1. Assumptions may be used as assertions in another context.
#2. Assertions may be used as assumptions to prove another assertion.
#3. Specifying which assumptions/constraints to include/exclude for
proving a property has value.
Thanks Erich;
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Sep 13 2002 - 08:14:59 PDT