Hierarchical Verication of the Implementation of The IEEE-754 Table-Driven Floating-Point Exponential Function using HOL

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