Formal proof of integer adders using all-prefix-sums operation

DOI10.1007/S11432-011-4331-7zbMATH Open1270.65086OpenAlexW2256816214MaRDI QIDQ362271FDOQ362271

Authors: Qingping Tan, Otmane Ait Mohamed, Feng Liu 

Publication date: 20 August 2013

Published in: Science China Information Sciences (Search for Journal in Brave)

Full work available at URL: http://engine.scichina.com/doi/10.1007/s11432-011-4331-7

Recommendations

• Formal proof of prefix adders
• Functional verification of high performance adders in \textsc{Coq}
• scientific article; zbMATH DE number 1670746
• scientific article; zbMATH DE number 139976
• A proof of the nonrestoring division algorithm and its implementation on an ALU

zbMATH Keywords

VLSIcomputer arithmeticinteger adderprefix computationsemi-group

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Numerical algorithms for computer arithmetic, etc. (65Y04)

Cites Work

• Title not available (Why is that?)
• 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
• FUNCTIONAL PEARL Derivation of a logarithmic time carry lookahead addition circuit
• Proofs of Correctness and Properties of Integer Adder Circuits
• A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations

Cited In (3)

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

This page was built for publication: Formal proof of integer adders using all-prefix-sums operation

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