<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>7055</REFNUM><AUTHORS><AUTHOR>O'Donnell,J.T.</AUTHOR><AUTHOR>Ruenger,G.</AUTHOR></AUTHORS><YEAR>2001</YEAR><TITLE>Derivation of a carry lookahead addition circuit</TITLE><PLACE_PUBLISHED> Proc. ACM SIGPLAN Haskell Workshop (HW2001), Electronic Notes in Theoretical Computer Science, Vol. 59, No. 2 </PLACE_PUBLISHED><PUBLISHER>Electronic Notes in Theoretical Computer Science</PUBLISHER><LABEL>O'Donnell:2001:7055</LABEL><KEYWORDS><KEYWORD>binary addition</KEYWORD></KEYWORDS<ABSTRACT>Using Haskell as a digital circuit description language, we transform a ripple carry adder that requires O(n) time to add to n-bit words into an efficient carry lookahead adder that requires O(log n) time. The main difficulty is that the ripple carry adder uses a scan function to calculate carry bits, but this scan cannot be parallelised directly since it is applied to a non-associative function. Several additional techniques are needed to circumvent this problem, including partial evaluation and symbolic function representation. The derivation given here is suitable for a formal correctness proof, yet it also makes the solution more intuitive by bringing out explicitly each of the ideas underlying the carry lookahead adder. </ABSTRACT></RECORD></RECORDS></XML>