Subject: [sv-ac] RE: R44c - assume/check either, neither; must/should/could.
From: Erich Marschner (erichm@cadence.com)
Date: Thu Sep 12 2002 - 12:59:26 PDT
Hi Adam,
I think the problem here is that there are many scenarios, any of which is reasonable. This is why I'd prefer to state the meaning of 'assert' and 'assume' abstractly, so that we focus on the essential semantics and not over-constrain an implementation.
Here are some of the scenarios:
1. Formal verification, properties described outside the design (whether the design is hierarchical or flat):
In this case, the designer (or architect) may need to explicitly specify what assumptions are required to prove a given assertion. And then in the next step, an assertion proven may be used as an assumption to prove something else - with care to avoid circular reasoning.
2. Formal verification, properties described in the design (embedded in a given module) - "assert" can be used for properties that should be provable given the module and any constraints on its inputs; "assume" is the only reasonable thing to say about constraints on inputs. When the module is instantiated at a higher level, "assumes" in the instantiated module may become provable in the larger context, so either the designer has to edit the module to change "assume" to "assert" (not a good flow), or the tools should understand that "assume"s that can be verified, should be - in which case the difference between "assume" and "assert" becomes somewhat nebulous, other than the fact that "assume" refers to the external environment and "assert" refers to the module.
3. Simulation, properties described wherever - "assert" seems to be clearly a property that should be checked, but "assume"s (on inputs) could either be checked (to make sure the test bench is driving correctly) or could be implemented as constraints in a constrained random vector generation scheme.
The key difference between "assert" and "assume" seems to be that "assert" consistently expresses the designer's intent that a particular property should hold (and therefore should be verified), but "assume" may be interpreted as "assume" or "assert" or "generate" in different situations, depending upon what tool is being used, and how the tool handles hierarchy.
As I mentioned, the Sugar PSL definition reflects this. Here are the relevant definitions from the LRM:
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.
| So, are formal tools the only ones that adhere to the meaning of
| assume and check? If a simulation tool does not have to adhere, do
| we need to require a specific set of tools to do so?
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.
| [I presume this discussion doesn't include assumptions that are
| intended to simplify property verification and are not inclusive
| of the complete behavior - these wouldn't hold in simulation and
| would have to be excluded, turned off, etc.]
On the contrary, they might well hold in simulation. Remember that a typical test bench will not stimulate all possible behaviors of the design - in fact, one way to constrain the verification process is to write a simulation test bench for a specific scenario. And one way to define such a scenario might be to write assumptions (including sequential assumptions).
| Is is acceptable to say that check/assume mean something, but that
| tools may choose to do more than the definition? I had heard
| talk that this is not acceptable, because properties then may not
| transfer from tool to tool.
Assertions express properties that are expected (or assumed) to hold, regardless of what tool is used to check this or make this true. To that extent, assertions will transfer between tools. But I don't think we can hope to guarantee that the way in which properties are checked, or made to hold, will transfer from one tool to the next. That would amount to standardizing tool user interfaces, and I don't think that is possible.
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
| -----Original Message-----
| From: Adam Krolnik [mailto:krolnik@lsil.com]
| Sent: Thursday, September 12, 2002 3:06 PM
| To: Erich Marschner
| Cc: sv-ac@eda.org
| Subject: R44c - assume/check either, neither; must/should/could.
|
|
|
|
|
| Hi Erich;
|
|
| You are asking in this requirement if assume/check really needs
| to be specified for a property, or whether one just needs something
| that says, 'USE' this property?
|
| Presumably you are asking this because to one module an assumption
| (on a set of signals) is something that must be satisfied
| externally.
| But for another module (say the one connected and producing the
| signals) it could be/should be a requirement.
|
| It is interesting that a simulation tool could intepret both
| assume and check as directives to ensure the simulation satisfies
| this property.
|
| So, are formal tools the only ones that adhere to the meaning of
| assume and check? If a simulation tool does not have to adhere, do
| we need to require a specific set of tools to do so?
|
| [I presume this discussion doesn't include assumptions that are
| intended to simplify property verification and are not inclusive
| of the complete behavior - these wouldn't hold in simulation and
| would have to be excluded, turned off, etc.]
|
| Is is acceptable to say that check/assume mean something, but that
| tools may choose to do more than the definition? I had heard
| talk that this is not acceptable, because properties then may not
| transfer from tool to tool.
|
|
| What do others think? Should we have assume/check/prove?
|
| Adam Krolnik
| Verification Mgr.
| LSI Logic Corp.
| Plano TX. 75074
|
This archive was generated by hypermail 2b28 : Thu Sep 12 2002 - 13:01:38 PDT