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

rder 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.

• Type: Journal
• Year: 2010
• Where: CJ
• Authors: Behzad Akbarpour, Amr T. Abdel-Hamid, Sofiène Tahar, John Harrison
• Keywords: CJ 2010, HOL Verification, Rder Logic, Verification Task