论文部分内容阅读
Addition of two binary numbers is a fundamental operation in electronic circuits.Several integer adder architectures have been proposed.Their formal properties are well known,but the proofs are either incomplete or difficult to find.In this paper,we present a formal proof for the correctness of prefix adders.Both sequential and parallel algorithms are formalized and proved.In contrast to previous proofs using higher order functions and rewriting systems,our work is based on first order recursive equations,which are familiar to the computer arithmetic community and are therefore understandable by people working on VLSI circuit design.This study sets up a basis for further work on formal proofs of computer arithmetic algorithms.
Addition of two binary numbers is a fundamental operation in electronic circuits. Several integer adder architectures have been proposed. Their formal properties are well known, but the proofs are either incomplete or difficult to find.In this paper, we present a formal proof for the correctness of prefix adders.Both sequential and parallel algorithms are formalized and proved. In contrast to previous proofs using higher order functions and rewriting systems, our work is based on first order recursive equations, which are familiar to the computer arithmetic community and are therefore understandable by people working on VLSI circuit design. This study sets up a basis for further work on formal proofs of computer arithmetic algorithms.