Subject: RE: Assume-guarantee support
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 16 2001 - 12:38:21 PDT
Hi Hillel,
What you describe below is a very general question.
In FTL, there is no need to convert the assertions of B, C, D into
assumptions. Exactly
the same properties can be used. And no, we do not necessarily need a
complete
environment for A - we need only the assumptions on which the property at
hand is
dependent. As for the assumptions on B, C and D, in most cases we will not
need them
if the correct properties were written (and proven) on B, C, D.
Roy
-----Original Message-----
From: hillel miller [mailto:hillelm@msil.sps.mot.com]
Sent: Monday, July 16, 2001 8:42 PM
To: Armoni, Roy
Cc: Hillel Miller (r53776); vfv@eda.org
Subject: Re: Assume-guarantee support
Roy,
What I am trying to understand is the Forspec methodology as far as
assume/guarantee is concerned.
How are asserts reused as assumes within this methodology ?
For example, we could have one block 'A' with 3 neighbouring blocks (B,
C and D) for which asserts have been written. A is driven by B, C, D.
Is the methodology to convert the assertions of B, C, D into
assumptions,
giving us a complete environment for A ? What about the original
assumptions
of B, C and D. How are they taken into account ?
Hillel
"Armoni, Roy" wrote:
> 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 16 2001 - 12:39:03 PDT