Subject: Assume/Guarantee completeness - More Important than Advertised
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Aug 02 2001 - 00:47:10 PDT
Hi Danny,
I think that I already mentioned in the past that for bug hunting, A/G does
not add much.
However, for building proof it is a very important capability and is
essential if no other
tools are given.
The method that you describe below is called case-splitting, and it is
indeed good for
bug hunting. It might be that in IBM's methodology you do not want to build
proof. Another
possibility is that Sugar does not decently support A/G which leads its
users to end up
with only bug hunting. However, Intel's methodology requires A/G [See Bob
Bentley's talk
in DAC'01] and knows how to benefit from it. Actually, I am amazed by the
portion of the
Pentium 4 for which our users succeeded to prove formally! Thus, arguing
the A/G is not
usable is simply incorrect.
Roy
-----Original Message-----
From: Danny Geist [mailto:GEIST@il.ibm.com]
Sent: Wednesday, August 01, 2001 10:42 PM
To: vfv@eda.org
Subject: Assume/Guarantee completeness - Not Important as Advertised
There has been a very long discussion about the importance of completeness
of A/G.
I want to pose a different view which is more practical, and is derived
from real usage.
Our user community has a verification methodology which is somewhat in
contradiction with the assert/assume methodology. Accordingly, at least
for the wide user community that we work with, Assume/Guarantee is, at
best, a "nice to have". Definitely not a "strong requirement". I would
further argue that the same holds for any mainstream user community.
Here's why:
The biggest problem in Model Checking (MC) is state explosion.
Unfortunately, as much as we have tried through the years to
conceal it from users, they are still quite exposed to it and
in fact they find themselves continuously fighting it. One of
the most common methods of fighting state-space explosion is by
running properties with different environments, e.g. run the
property where the Unit Under Verification (UUV) in presented
only with"read" requests, and afterwards run the same property
where the UUV is presented only with "write" requests. Of course,
this is not verification - it is refutation. But that's where the
state of the practice is now - its the best way to hunt bugs.
That's why people use MC. The above methodology is very widespread
and successful amongst practitioners.
Continuing the above argument using our example UUV, obviously we
DON'T try to prove that the adjacent block that supplies the
"read/write" always does just "reads" or just "writes". It's not
true because the adjacent block DOES mix them up. As I will show
in the sequel, this is there where the A/G methodology breaks down...!
The only way to make A/G work, in light of the latter observation,
is to make the UUVs we verify so small that we can have the most
general LEGAL environment for them without exploding. In most cases,
that is totally uneconomical in terms of manpower. It means that
users capture too small a part of the entire design in one session,
not to mention the effort in learning interfaces deep inside the
chip (the boundaries of the very small UUV). In other words, you
can only do "pure" A/G a very small percentage of the time.
So the point I am trying to make here is: It's NOT that important
that every specification will be able to be assumed, because for
most of them the A/G methodology breaks down for reasons of state
explosion. It's much more important that users have all the language
constructs they need in order to be productive!!
To summarize, it seems that insisting on the "Completeness of the A/G of
the property language" means paying a price in language usability and dont
get me wrong I think its a good thing to have completeness its just not
a requirement and it can hurt.
Finally, I think the discussion is moving along too quickly and in
my opinion unprofessionally. This discussion should not be about
choosing one language or another... it should be about constructing
a good and usable language for property specification.
Regards,
Danny
Daniel Geist
IBM Haifa Research Lab. Phone:
972-4-8296286
MATAM - Advanced Technology Center Fax: 972-4-8296112
Haifa, ISRAEL
e-mail: geist@il.ibm.com
This archive was generated by hypermail 2b28 : Thu Aug 02 2001 - 07:58:41 PDT