Members

• Amr Abdel-Hamid
• Dr. Sofiène Tahar
• John Harrison

Description

The IEEE-754 floating-point formats have become a standard in the representation of real numbers. Numerous mathematical functions have been designed to manipulate these numbers and perform such transcendental arithmetic operations as addition, multiplication, logarithm, exponential etc. 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. The goal for this project is to perform formal verification on a mathematical function, namely the exponential function, and show that the VHDL/Verilog implementation satisfies the proposed algorithm. The verification will be conducted using the theorem prover HOL (Higher-Order Logic). We adopted a hierarchical verification approach allowing us to tackle the complexity of the IEEE-754 floating-point exponential function. 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. we have used both hierarchical and modular approaches for modeling and verifying the floating-point exponential function in HOL. We are connecting the previously built proof to the mathematical proof build by J. Harrison, aiming to achieve a proof for the whole design path of the circuit.

Publications

1. T. Abdel-Hamid, S. Tahar, and J. Harrison: Enabling Hardware Verification through Design Changes; In: C. George, H. Miao (Eds.), Formal Methods in Software Engineering, Lecture Notes in Computer Science 2495, Springer Verlag, 2002, pp. 459-470. Proc. International Conference on Formal Engineering Methods (ICFEM'02), Shanghai, China, October 2002.
2. A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL ; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'2001), Edinburgh, Scotland, UK, September 2001.
3. H. T. Bui and S. Tahar: Design and Synthesis of an IEEE-754 Exponential Function ; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), Edmonton, Alberta, Canada, May 1999. pp. 450-455.
4. H.T. Bui, B. Khalaf and S. Tahar: Table-Driven Floating-Point Exponential Function ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1998. [19 pages]
5. Amr Talaat Abdel-Hamid: A Hierarchical Verification of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL . M.A.Sc. Thesis, Concordia University, Department of Electrical and Computer Engineering June 2001.