Sponsor
This work has been supported by the National Science Foundation of China Grant 61272002, the Tsinghua National Laboratory for Information Science and Technology (TNList) Cross-discipline Foundation 2011-9, the Major Research plan of the National Natural Science Foundation of China Grant 91218302, and the National Basic Research Program of China (973 Program) Grant 2010CB328003.
Published In
Journal of Applied Mathematics
Document Type
Article
Publication Date
2014
Subjects
Automatic theorem proving, calcul construction, COQ
Abstract
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.
DOI
10.1155/2014/197252
Persistent Identifier
http://archives.pdx.edu/ds/psu/11547
Citation Details
Qian Wang, Xiaoyu Song, Ming Gu, and Jiaguang Sun, “Functional Verification of High Performance Adders in COQ,” Journal of Applied Mathematics, vol. 2014, Article ID 197252, 9 pages, 2014.
Description
This is the publisher's final PDF. The article was originally published in Journal of Applied Mathematics and can be found online at: http://www.hindawi.com/journals/jam/2014/197252/
Copyright © 2014 Qian Wang et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.