Subject: Assume-guarantee support
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 09 2001 - 21:43:11 PDT
Hi Hillel,
I am changing the subject of this thread - I do not think that we
talk about Sugar complexity here anymore. Hope you agree.
Please see my answers below.
Regards, Roy
> Roy,
>
> Other things that are of concern are :
> How the user uses the assume/guarantee ?
It is in ForSpec reference manual, but to save you the burden of
finding, then it looks like that:
assert f; // if you want to guarantee f
assume f; // if you want to assume f
> How the user is taught to use assume/guarantee ?
Well, given that all one needs is to learn to use either
"assert" or "assume", there is not much to teach here from
the language point of view.
> Why is the general assertion approach better than the
> restrict(Sugar)/constraint(CBV)+
> DFSM approach ?
I'm not sure that I fully understand what happens in Sugar
and CBV. What exactly can be assumed and what not? How the
users are taught what is a legal assumption? What is the
expressive power of assumptions? Is it possible to express
every property of the design as an assumption and is it
possible to later guarantee that property without the need to
rewrite it in a different way?
In FTL we have a clear understanding of what is the expressive
power of the formulae and we can answer all the above
questions positively. More details are in the document that
I am preparing.
> What debugging capabilities exist ?
Is this about tools and methodology? If not, kindly clarify
this question.
> How this works in the dynamic world ?
Again, this is explained in the reference manual, but I
will repeat it here. Our approach to assumptions is that
these properties specify things that really hold in the
full chip. Thus, in simulation where we also have the
environment in which the assumptions need to hold, there is
no point in using them as assumptions. Since the environment
exists, we simply check that they really hold. So the
short answer should be that in simulation assumptions are
treated the same way as assertions.
This archive was generated by hypermail 2b28 : Mon Jul 09 2001 - 21:44:18 PDT