Subject: RE: [sv-ac] R44c - assume/check either, neither; must/should/could.
From: Richard Ho (rho@0-in.com)
Date: Thu Sep 12 2002 - 12:47:49 PDT
Apologies if I missed the conference call discussion on
this topic.
I would just like to point out that there are places
where a user would want to group together sets of properties
with assume/check directives. For example, when writing
properties for a standard bus interface.
There are some properties which need to be marked as
assumptions. It can be argued that tools can infer which
properties are supposed to be assumptions, but in general,
it is easy for the user to declare them. When writing
properties that are meant to be re-used, the ability to
capture the verification directive (assume/check) can be
valuable in some places. This provides an assurance that
tool interpretations will be the same for certain assumptions.
Note that I am only making this point in relation to
requirement R44a - which says that the user is given no
ability to specify the directive. I believe that this
requirement is too strong.
By the way, what is the difference between R44c and R45*?
Best regards,
Richard.
----------------------------------------------------------------------
Richard C. Ho (rho@0-in.com) Tel: 408-487-3647
http://www.0-in.com Fax: 408-487-3651
0-In Design Automation, Inc, 1784 Technology Drive, San Jose, CA 95110
| -----Original Message-----
| From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On
| Behalf Of Prakash Narain
| Sent: Thursday, September 12, 2002 12:20 PM
| To: sv-ac@eda.org
| Subject: Re: [sv-ac] R44c - assume/check either, neither;
| must/should/could.
|
|
| Adam,
|
| My argument is that in a non-hierarchical view of the design,
| constructs
| like
| assume/check makes sense. In a hierarchical view of the design, where
| assume/check will be encountered in changing contexts depending upon
| the position in the hierarchy, we need clear semantics of how
| to interpret
| these constructs.
|
| In any case, these constructs address tool control issues.
| That can be
| accomplished by naming assertions and using names in tool
| control scripts.
|
| Best Regards,
|
| Prakash
|
| Adam Krolnik wrote:
|
| >
| >
| >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 - 12:49:00 PDT