Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq

Author

Qian Wang ; Xiaoyu Song ; Hung, W.N.N. ; Ming Gu ; Jiaguang Sun

Author_Institution

Sch. of Software, Tsinghua Univ., Beijing, China

Volume

34

Issue

1

fYear

2015

fDate

Jan. 2015

Firstpage

150

Lastpage

154

Abstract

Theorem proving has been demonstrated as a powerful technique for datapath verification. This paper considers a generic logic-level architecture of end-around-carry adder, which is extensively used in floating-point arithmetic. The architecture is component-based and parameterized for easy customization. The design architecture is formalized and verified in the mechanical theorem prover Coq. The scalable proof provides necessary underpinnings for verifying customized and new implementations.

Keywords

adders; floating point arithmetic; logic testing; Coq floating point units; datapath verification; floating point arithmetic; generic end around carry adder; logic level architecture; scalable verification; Abstracts; Adders; Arrays; Educational institutions; Indexes; Lenses; Architecture; Coq; End-around-carry adder; architecture; end-around-carry adder (EAC); floating-point unit; floating-point unit (FPU); portable; theorem proving; verification;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/TCAD.2014.2363391

Filename

6926810