The Pentium chip wasn't verified

Miriam Leeser (mel@ultrastar.EE.CORNELL.EDU)
Mon, 21 Nov 94 11:59:14 EST

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