A mechanically-validated technique for extending the available precision

Some floating-point applications use 64 bit double precision numbers but it is difficult to find a fast, cheap and small DSP-unit on such a precision. We propose to extend the available precision to any length and specially to create double precision arithmetic with a 32 bit single precision unit. We have developed algorithms and formal proofs of the addition, the multiplication and the division. The proofs have been checked with the Coq automatic proof checker. As a DSP may control a critical process, these proofs help build confidence in the program correctness.