Login | Register

Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL

Title:

Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL

Akbarpour, B., Abdel-Hamid, A. T., Tahar, Sofiène and Harrison, J. (2010) Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. The Computer Journal, 53 (4). pp. 465-488. ISSN 0010-4620

[img]
Preview
Text (application/pdf)
CJ-2010.pdf - Accepted Version
229kB

Official URL: http://dx.doi.org/10.1093/comjnl/bxp023

Abstract

Deep datapath and algorithm complexity have made the verification of 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 paper, we have hierarchically formalized and verified a hardware implementation of the IEEE-754 table-driven floating-point exponential function algorithm using the higher-order logic (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 gate-level implementation of the circuit up to a high-level mathematical specification.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Akbarpour, B. and Abdel-Hamid, A. T. and Tahar, Sofiène and Harrison, J.
Journal or Publication:The Computer Journal
Date:2010
Digital Object Identifier (DOI):10.1093/comjnl/bxp023
ID Code:977365
Deposited By: DANIELLE DENNIE
Deposited On:14 Jun 2013 14:05
Last Modified:18 Jan 2018 17:44
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

Back to top Back to top