Subject: RE: Practical assume/guarantee
From: Armoni, Roy (roy.armoni@intel.com)
Date: Tue Dec 04 2001 - 07:17:16 PST
Hi Bernard,
Let me start from the end of your mail, and admit that indeed the property
document tells only part of the story. I tend to think that the most
important
thing is the methodology. The language and the tools are merely enablers
for implementing the methodology. Intel has agreed to donate to the
industry
only the language; neither the tools, nor the methodology are part of this
donation. That is why I cannot say too much about A/G in Intel.
Nevertheless, let me mention a few things about methodology. I believe that
the most common paradigm in validation is "bug hunting". The reason is that
this is basically what you can achieve in simulation. That is why most FV
users actually do bug hunting, because they are measured by the number of
bugs they find (for the designer, bugs are bad. for the validator, bugs are
good).
So I cannot see how we can design a standard that does not allow bug
hunting.
A different methodology than bug hunting could be to prove properties. For
that, we should look back at how we prove theorems in mathematics. One
theorem may require a few lemmas, which in turn require additional lemmas
to be proven. The A/G paradigm employs a similar scheme. The point is that
one needs to be very careful about choosing the lemmas that will assist in
proving the theorem. If they are too strong, the theorem will be proven,
but it
will not be possible to prove the lemmas. If they are too weak, it would be
possible to prove the lemmas but they will not imply the theorem. The point
that I am trying to make is that it is important that your properties will
really
capture the intention.
Now, as for ForSpec, last July I sent out a document that formalizes what is
required to fully support the A/G paradigm. It contains definitions of
soundness,
completeness and tractability with respect to A/G. It also contains a very
accurate statement of why ForSpec fully supports the A/G paradigm. I also
would like to iterate that every ForSpec formula may be assumed and/or
asserted. Only that it is important to carefully understand what the
formula
mean (and I showed in the above mentioned document that any logic that
assumes universal quantification over the initial states or over the traces,
including LTL and CTL may be misused to specify "interesting" cases).
Regards,
Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Friday, November 30, 2001 8:16 PM
To: roy.armoni@intel.com
Cc: vardi@cs.rice.edu; vfv@eda.org; Cindy Eisner
Subject: Practical assume/guarantee
At 05:48 AM 11/29/2001 -0600, Moshe Vardi wrote:
>I just want to know to what extent Repackaged Sugar supports the
>assume-guarantee approach. What can be assumed and what can be
>guaranteed relative to what assumptions?
Roy,
I guess I should direct my questions towards you, as I assume you have more
practical experience of the use of assume/guarantee, compared to their
theoretical implications.
It's interesting that Moshe raises assume/guarantee because I've recently
been wondering about the real, practical value of this approach. It's been
claimed that ForSpec has almost 100% support for the assume/guarantee
paradigm, though if you look at, for example, property #12 there is a clear
implication some assertions cannot be assumed. I confess I have no
understanding of why this should be the case, though there was an earlier
agreement between you and Cindy that there was at least one case which was
fundamentally impossible.
As I understand it ForSpec assumptions form the environment constraints
against which assertion checks are made. Is this correct?
My limited knowledge of real Formal Model checkers suggests the user
typically has to restrict (reduce) the operating assumptions for the model
in order to alleviate size issues. One concern I have therefore is if he
has to restrict the operating area for one block, just how practical can
the interchange of rules between assume & guarantee modes be? Will he
always be willing and able to restrict each block in an identical manner?
Also, how does a user segment the assumptions and the assertions where
there are complex interaction between 3 or more blocks. Is this *really*
possible in practice?
And how does the user dictate environmental constraints like the reset has
to be active for 5 cycles, that would not always be verified by assertion
on the adjacent block?
Perhaps I'm showing my ignorance here but, widening the picture to look at
all the donated languages, it seems I don't really have a very good picture
of how much the different donated languages suppose the environmental
constraints against which the model checks are described. My belief is:
a) Sugar requires code written in edl to establish the environment
b) ForSpec relies on the assume/guarantee, therefore (presumably?) ForSpec
assertions are written about the interface signals to establish the
operating conditions for a design under verification
c) CBV assumptions/constraints are written in CBV
d) I'm not clear about how it is proposed temporal 'e' should handle this
issue
I thought the property document very illuminating, however I'm beginning to
realise this only tells part of the story. We run a risk of straying from
language into the implementation within individual tools, however is there
a way we can establish how much the design of a language imposes on the
tools in this area? And how practical the different approaches are in
practice? Has anyone benchmarked them all on the same models? Would it be
feasible to do this? Alternatively, does anyone out there have enough
experience to comment on the practical differences between the overall
solutions?
Thanks
Bernard
====================================================================
SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
431-5126
Email: bdeadman@sdvinc.com Website: www.sdvinc.com
This archive was generated by hypermail 2b28 : Tue Dec 04 2001 - 07:18:30 PST