Login | Register

A hierarchical verification of the IEEE-754 table-driven floating-point exponential function using HOL

Title:

A hierarchical verification of the IEEE-754 table-driven floating-point exponential function using HOL

Abdel-Hamid, Amr Talaat (2001) A hierarchical verification of the IEEE-754 table-driven floating-point exponential function using HOL. Masters thesis, Concordia University.

[thumbnail of MQ64057.pdf]
Preview
Text (application/pdf)
MQ64057.pdf
2MB

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 thesis, we have formalized and verified a hardware implementation of the IEEE-754 Table-Driven floating-point exponential function algorithm 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

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Abdel-Hamid, Amr Talaat
Pagination:viii, 65 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:2001
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:QA 76.9 C62A23 2001
ID Code:1485
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:19
Last Modified:13 Jul 2020 19:49
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top