language: en

Verifying adder circuits using powerlists

William Adams
Department of Computer Sciences The University of Texas at Austin
Austin, TX 78712-1188 USA
e-mail: will@cs.utexas.edu March 29, 1994

Abstract We define the ripple-carry and the carry-lookahead adder circuits in the powerlist notation and we use the powerlist algebra to prove that these circuits correctly implement addition for natural numbers represented as bit vectors.

0 Introduction