Functional Verification of High Performance Adders in C OQ

Qian Wang, Xiaoyu Song, Ming Gu and Jiaguang Sun

Journal of Applied Mathematics, 2014, vol. 2014, 1-9

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 C OQ . 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.

Date: 2014
References: Add references at CitEc
Citations:

Downloads: (external link)
http://downloads.hindawi.com/journals/JAM/2014/197252.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2014/197252.xml (text/xml)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hin:jnljam:197252

DOI: 10.1155/2014/197252

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().