EECS 298-11: CAD Seminar
Wednesday, April 10, 1996, 5pm
531 Cory Hall, Hogan Room


		 Modular Verification of SRT Division

		       M. Srivas and N. Shankar
	       SRI International Computer Science Lab.
       (Joint work with Harald Ruess of the University of Ulm)

The SRT division algorithm is a popular method for implementing
high-performance floating-point division.  In order to compute the
partial remainder and quotient digit in parallel, the SRT algorithm
exploits a redundant number representation and a large table of
precomputed values to carefully estimate each quotient digit from
approximations of the partial remainder and the divisor.  The
algorithm poses some interesting challenges for verification.  For
instance, the finite-state approaches based on BDDs cannot easily
handle the correctness of nontrivial arithmetic operations.
Extensions of these methods also have serious limitations.  We show
how it is possible to use the PVS specification language and proof
checker to present an elegant formalization of the mathematics
underlying the algorithm for an arbitrary radix, and an instantiation
of this algorithm that yields the correctness of a specific
implementation.  We first give an informal description of the
algorithm and then show how the various features of PVS can be used to
obtain a readable, high-level specification.  The verification
exploits the tight integration between rewriting, arithmetic decision
procedures, and equality, that is present in PVS.  The main thesis of
this talk is that techniques based on high-level specification and
highly automated formal proof checking can and should be used in the
verification of complex computer arithmetic circuits.


Upcoming seminars:

April 8 (Monday): Henry Verheyen, Aptix Corp.

April 17: John Cohn, IBM

April 22 (Monday):  Henny Sipma and Tomas Uribe, Stanford

April 24:  Fong Pong, Sun Microsystems