Functional Verification of High Performance Adders in COQ
Joint Authors
Gu, Ming
Sun, Jiaguang
Wang, Qian
Song, Xiaoyu
Source
Journal of Applied Mathematics
Issue
Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-9, 9 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2014-04-10
Country of Publication
Egypt
No. of Pages
9
Main Subjects
Abstract EN
Addition arithmetic design plays a crucial role in high performance digital systems.
The paper proposes a systematic method to formalize and verify adders in a formal proof assistant COQ.
The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way.
The methodology can be extended to other adder architectures as well.
American Psychological Association (APA)
Wang, Qian& Song, Xiaoyu& Gu, Ming& Sun, Jiaguang. 2014. Functional Verification of High Performance Adders in COQ. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-453769
Modern Language Association (MLA)
Wang, Qian…[et al.]. Functional Verification of High Performance Adders in COQ. Journal of Applied Mathematics No. 2014 (2014), pp.1-9.
https://search.emarefa.net/detail/BIM-453769
American Medical Association (AMA)
Wang, Qian& Song, Xiaoyu& Gu, Ming& Sun, Jiaguang. Functional Verification of High Performance Adders in COQ. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-453769
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-453769