From owner-qed Mon Nov 21 11:02:49 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA20976 for qed-out; Mon, 21 Nov 1994 10:59:36 -0600 Received: from ultrastar.EE.CORNELL.EDU (ULTRASTAR.EE.CORNELL.EDU [128.84.240.36]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA20970 for ; Mon, 21 Nov 1994 10:59:28 -0600 Date: Mon, 21 Nov 94 11:59:14 EST From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser) Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) id AA18857; Mon, 21 Nov 94 11:59:14 EST Message-Id: <9411211659.AA18857@ultrastar.EE.CORNELL.EDU> To: beeson@cats.UCSC.EDU Cc: qed@mcs.anl.gov In-Reply-To: beeson@cats.UCSC.EDU's message of Sat, 19 Nov 1994 22:44:10 -0800 <199411200644.WAA12756@si.UCSC.EDU> Subject: The Pentium chip wasn't verified Sender: owner-qed@mcs.anl.gov Precedence: bulk In hardware verification, arithmetic circuits is an application area where theorem proving has advantages over other automated techniques, such as those based on model checking. Despite the advantages, there has not been a lot of research on verifying the kinds of floating point circuits that appear in high performance processors such as the Pentium. The Pentium uses a subtractive division algorithm based on a radix-4 Booth SRT algorithm. Similar algorithms are used for square root and division in this and several other processors. We have a proof of a radix 2 subtractive square root chip. The paper describing this proof appeared in the Conference on Theorem Provers in Circuit Design in September 1994. We are working on a proof of a radix 2 subtractive division implementation. The two proofs are very similar. Verification of radix 4 is somewhat more difficult, largely because the implementation depends on a lookup table to guess the next digit. We have also done an analysis and comparison of floating point divide and square root implementations in high-performance microprocessors. These include Pentium, DEC Alpha, HP 7100 and MIPS R4000. A technical report based on this work should be available in about 2 weeks time. References on the Pentium: Alpert and Avnon, "Architecture of the Pentium Microprocessor". IEEE Micro pgs 22-35, June 1993. Case, "Intel reveals Pentium implementation details: Architectural enhancements remain shrouded by NDA". Microprocessor Report, pgs 9-17, March 1993. Miriam Leeser mel@ee.cornell.edu