Subject: RE: Puzzled - please explain
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sun Aug 12 2001 - 00:04:09 PDT
Hi Bernard,
The discussion was about A/G - not about ForSpec.
Do you have data of any other project in which 10,000 properties were proved
formally?
In my mind, it is amazing!
Regards, Roy
-----Original Message-----
From: Bernard Deadman [mailto:bdeadman@sdvinc.com]
Sent: Thursday, August 09, 2001 10:07 PM
To: Armoni, Roy
Cc: 'Danny Geist'; vfv@eda.org
Subject: Puzzled - please explain
At 10:47 AM 8/2/2001 +0300, Armoni, Roy wrote:
Roy,
You wrote:
>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.
but Bob Bentley, when I asked him about his experiences with ForSpec wrote:
>From: "Bentley, Bob" <bob.bentley@intel.com>
>To: "'Bernard Deadman'" <bdeadman@sdvinc.com>
>Subject: RE: Formal Verification
>Date: Wed, 8 Aug 2001 11:23:46 -0700
>X-Mailer: Internet Mail Service (5.5.2653.19)
>
>Bernard,
>
>We did not use ForSpec as part of the Pentium 4 processor validation
>program, either for Formal Verification or as a coverage tool for dynamic
>verification, so I don't have any experience with the language.
>
>Regards,
>
>Bob.
If I look again at Bob's DAC paper he mentions the "prover" tool and "FSL"
and, while he mentions verification of blocks, he does not ever, as you
imply from your reference to his paper, even mention Assume/Guarantee let
alone state its importance.
Also, in his paper Bob states that Formal Verification was used for two
significant segments of the design (the FPU and the instruction decoder)
but I don't think this would be even half the 'gates' in the device
(actually I think it might be equivalent to what Bob describes as a
"cluster" ie 1/6th or 1/7th of the total machine), so your statement that
"I am amazed by the portion of the Pentium 4 for which our users succeeded
to prove formally" paints an optimistic picture in my mind.
I don't doubt you have good experiences with users, but I'm very confused
about how much was achieved by ForSpec and A/G in the verification of the
Pentium 4. Could you please clarify this for me?
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 : Sun Aug 12 2001 - 00:09:25 PDT