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

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

IEEE Trans. on CAD of Integrated Circuits and Systems（2015）

引用 2|浏览24

暂无评分

摘要

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.

查看译文

关键词

adders,Architecture,floating-point unit,Coq,end-around-carry adder,coq floating point units,verification,architecture,End-around-carry adder,end-around-carry adder (EAC),scalable verification,theorem proving,datapath verification,floating-point unit (fpu),logic level architecture,end-around-carry adder (eac),portable,Coq floating point units,floating-point unit (FPU),coq,generic end around carry adder,floating point arithmetic,logic testing

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要