##
Technical Report

###
**Hierarchical Verification of the Implementation of the IEEE-754
Table-Driven Floating-Point Exponential Function using HOL**

**A.T. Abdel-Hamid, S. Tahar, and J. Harrison**

**ABSTRACT**

The IEEE-754 floating-point standard, used in nearly all floating-point
applications, is considered one of the most important standards. Deep datapath
and algorithm complexity have made the verification of such floating-point
units a very hard task. Most simulation and reachability analysis verification
tools fail to verify a circuit with a deep datapath like most industrial
floating-point units. Theorem proving, however, offers a better solution
to handle such verification. In this report we have formalized and verified
a hardware implementation of the IEEE-754 Table-Driven floating-point exponential
function algorithm using the HOL theorem prover. The high ability of abstraction
in the HOL verification system allows its use for the verification task
over the whole design path of the circuit, starting from the gate level
implementation of the circuit up to a higher level behavioral specification.
To achieve this goal, we have used both hierarchical and modular approaches
for modeling and verifying the floating-point exponential function in HOL.