Functional verification of high performance adders in \textsc{Coq}
type: Item
instance of: scholarly article
title: Functional verification of high performance adders in \textsc{Coq}
zbMATH Open document ID: 1437.68191
DOI: 10.1155/2014/197252
author: Yanyan Li
published in: Journal of Applied Mathematics
publication date: 2019-11-19T00:00:00Z
review text: Summary: 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 \textsc{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.
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 94D10
zbMATH DE Number: 7131397
Wikidata QID: Q59050211
describes a project that uses: CoqMTU
describes a project that uses: Coq
describes a project that uses: PREVAIL
describes a project that uses: Coquet
MaRDI profile type: MaRDI publication profile
full work available at URL: https://doi.org/10.1155/2014/197252
OpenAlex ID: W2029501708
cites work: Hardware specification, verification and synthesis: mathematical aspects. Mathematical Sciences Institute workshop, Ithaca, NY, USA, July 5--7, 1989. Proceedings
cites work: Circuits as streams in Coq: verification of a sequential multiplier
cites work: Certifying circuits in type theory
cites work: Coquet: a Coq library for verifying hardware
cites work: FUNCTIONAL PEARL Derivation of a logarithmic time carry lookahead addition circuit
cites work: Formal proof of prefix adders
cites work: Mathematics of Program Construction
cites work: Q2958550
cites work: Computer arithmetic algorithms.
cites work: A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations
Recommended article: Formal proof of integer adders using all-prefix-sums operation
Recommended article: Automated and scalable verification of integer multipliers
Recommended article: Formal proof of prefix adders
Recommended article: A formal approach to designing multiple-valued arithmetic circuits
Recommended article: Formalization of fixed-point arithmetic in HOL
copyright license: Creative Commons Attribution 3.0 Unported
description: scientific article; zbMATH DE number 7131397