Sciweavers

TPCD
1994

Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization

13 years 4 months ago
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization
Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating di erent f abstraction. In this paper we show how a non-restoring integer square root algorithm can be transformed to a very e cient hardware implementation. The top level is a Standard ML function that operates on unbounded integers. The bottom level is a structural description of the hardware consisting of an adder subtracter, simple combinational logic and some registers. Looking at the hardware, it is not at all obvious what function the circuit implements. At the top level, we prove that the algorithm correctly implements the square root function. We then show a series of optimizing transformations that re ne the top level algorithm into the hardware implementation. Each transformation can be veri ed, and in places the transformations are motivated by knowledge about the operands that we can guarantee through veri cation. By decomposing the veri cation e ort ...
John W. O'Leary, Miriam Leeser, Jason Hickey, Mark
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1994
Where TPCD
Authors John W. O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard
Comments (0)