Hierarchical Approach for the Verification of an IEEE-754 Floating-Point Function
Amr Talaat Abdel-Hamid, Sofiène Tahar, John R Harrison · 1995
In this work, we have formalized and verified a hardware implementation of the Table-Driven algorithm for the floating-point exponential function. We have used a hierarchical approach enabling the verification of this function from the gate level implementation up to a behavioral specification adapted from the high level algorithmic description written by Harrison [3].