A mechanically-validated technique for extending the available precision

Author

Boldo, Sylvie ; Daumas, Marc

Author_Institution

Lab. de l´´Informatique du Parallelisme, ENS de Lyon, France

Volume

2

fYear

2001

fDate

4-7 Nov. 2001

Firstpage

1299

Abstract

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.

Keywords

digital signal processing chips; floating point arithmetic; 32 bit; 6 bit; Coq automatic proof checker; DSP; DSP units; addition; bit single precision unit; division; double precision arithmetic; double precision numbers; floating-point applications; mechanically-validated technique; multiplication; Arithmetic; Automatic control; Data structures; Digital signal processing; Hardware; History; Instruments; Internet; Mathematics; Process control;

fLanguage

English

Publisher

ieee

Conference_Titel

Signals, Systems and Computers, 2001. Conference Record of the Thirty-Fifth Asilomar Conference on

Conference_Location

Pacific Grove, CA, USA

ISSN

1058-6393

Print_ISBN

0-7803-7147-X

Type

conf

DOI

10.1109/ACSSC.2001.987700

Filename

987700