Formal proof of prefix adders

DOI10.1016/J.MCM.2010.02.008MaRDI QIDQ611751zbMATH OpenOpenAlexFDO

Authors Feng Liu, Qingping Tan, Gang Chen

Publication date 14 December 2010

Published in Mathematical and Computer Modelling (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.mcm.2010.02.008

zbMATH Keywords

VLSIcomputer arithmeticsemi-groupprefix adders

Mathematics Subject Classification ID

Hardware implementations of nonnumerical algorithms (VLSI algorithms, etc.) (68W35) Computability and recursion theory (03D99)

Recommendations

• Formal proof of integer adders using all-prefix-sums operation
• Functional verification of high performance adders in \textsc{Coq}
• scientific article; zbMATH DE number 1670746
• An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
• scientific article; zbMATH DE number 139976

Cites work

• A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations
• A Regular Layout for Parallel Adders
• A new class of parallel algorithms for finding connected components on machines with bit-vector operations
• Computer arithmetic algorithms.
• Mathematics of Program Construction
• Parallel Prefix Computation
• Proofs of Correctness and Properties of Integer Adder Circuits

Cited in

(3)

• Functional verification of high performance adders in \textsc{Coq}
• Formal proof of integer adders using all-prefix-sums operation
• scientific article; zbMATH DE number 5693751 (Why is no real title available?)

This page was built for publication: Formal proof of prefix adders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q611751)