Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 21 Nov 94 12:03:01 EST
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9411211703.AA18866@ultrastar.EE.CORNELL.EDU>
To: info-hol@leopard.cs.byu.edu
In-Reply-To: chou@cs.ucla.edu's message of Sun, 20 Nov 94 23:38:16 PST <9411210738.AA27152@maui.cs.ucla.edu>
Subject: FWD: The Pentium chip wasn't verified


I just sent this to the qed mailing list.  Since this topic is being
discussed here, I thought I would post it here too.  

This relates to Ching Tsun's question about verifying multipliers as
well.  I strongly believe that arithmetic circuits are a good
application area for theorem proving !!


*************************

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