Subject: [sv-ac] R44c - assume/check either, neither; must/should/could.
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Sep 12 2002 - 12:06:01 PDT
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:10:29 PDT