Subject: Re: [sv-ac] R44c - assume/check either, neither; must/should/could.
From: Prakash Narain (prakash@realintent.com)
Date: Thu Sep 12 2002 - 12:20:04 PDT
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:23:22 PDT