Han, JungangStone, Glen2008-05-202008-05-201988-07-01http://hdl.handle.net/1880/46505In this paper we first formulate the Conditional Sum Addition (CSA) algorithm, then design an area-time efficient Conditional Sum Adder in CMOS. We also design a Binary Look-ahead Carry adder and a fast ripple carry adder in the same technology for the comparison of their performances. Finally we formally prove that the CMOS implementation of the CSA adder is correct (i.e. the implementation meets the specification of the intended behavior) by using Mike Gordon's Higher Order Logic (HOL) system.EngComputer Scienceunknown1988-311-2310.11575/PRISM/31373