An FPGA Implementation of a Fully Verified Double Precision IEEE Floating-Point Adder

We report on the full gate-level verification and FPGA implementation of a highly optimized double precision IEEE floating-point adder. The proposed adder design incorporates many optimizations like a nonstandard separation into two paths, a simple rounding algorithm, unification of rounding cases for addition and subtraction, sign-magnitude computation of a difference based on one´s complement subtraction, compound adders, and fast circuits for approximate counting of leading zeros from borrow-save representation. We formally verify a gate-level specification of the algorithm using theorem proving techniques in PVS. The PVS specification was then used to automatically generate a gate-level implementation that was synthesized using Altera Quartus II. The resulting implementation has a total latency of 13.6 ns on an Altera Stratix II device.We have partitioned the design into a 2 stage pipeline running at a frequency of 147 Mhz.