Engineering design methodology recommends designing a system as follows: Start with an unambiguous speci cation, partition the system into blocks, specify the functionality of each block, design each block separately, and glue the blocks together. Verifying the correctness of an implementation reduces then to a local veri cation procedure. We apply this methodology for designing a provably correct modular IEEE compliant Floating Point Unit. First, we provide a mathematical and hopefully unambiguous de nition of the IEEE Standard which speci es the functionality. The design consists of: an adder, a multiplier, and a rounding unit, each of which is further partitioned. To the best of our knowledge, our design is the rst publication that deals with detecting exceptions and trapped over ow and under ow exceptions as an integral part of the rounding unit in a Floating Point Unit. Our abstraction level avoids bit-level arguments while still enabling addressing crucial implementation issues ...
Guy Even, Wolfgang J. Paul