Formal proof of prefix adders

DOI10.1016/J.MCM.2010.02.008zbMATH Open1201.68163OpenAlexW2087431822MaRDI QIDQ611751FDOQ611751

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

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 Keywords

VLSIcomputer arithmeticsemi-groupprefix adders

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

• Functional verification of high performance adders in \textsc{Coq}
• Title not available (Why is that?)

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)