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

Authors

Qian Wang, Tsinghua University
Xiaoyu Song, Portland State UniversityFollow
William N. N. Hung, Synopsys Inc.Follow
Ming Gu, Tsinghua UniversityFollow
Jiaguang Sun, Tsinghua UniversityFollow

Published In

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

Document Type

Citation

Publication Date

1-2015

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.

Locate the Document

https://doi.org/10.1109/TCAD.2014.2363391

DOI

10.1109/TCAD.2014.2363391

Persistent Identifier

http://archives.pdx.edu/ds/psu/19322

Citation Details

Q. Wang, X. Song, W. N. N. Hung, M. Gu and J. Sun, "Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 34, no. 1, pp. 150-154, Jan. 2015.