<XML><RECORDS><RECORD><REFERENCE_TYPE>10</REFERENCE_TYPE><REFNUM>7069</REFNUM><AUTHORS><AUTHOR>O'Donnell,J.T.</AUTHOR><AUTHOR>Ruenger,G.</AUTHOR></AUTHORS><YEAR>1995</YEAR><TITLE>A formal derivation of a parallel binary addition circuit</TITLE><PLACE_PUBLISHED>DCS Tech Report</PLACE_PUBLISHED><PUBLISHER>University of Glasgow</PUBLISHER><ISBN>TR-1995-19</ISBN><LABEL>O'Donnell:1995:7069</LABEL><KEYWORDS><KEYWORD>carry lookahead adder</KEYWORD></KEYWORDS<ABSTRACT>Formal equational reasoning is used to derive a binary addition circuit using a parallel tree topology from first principles: mathematical addition of natural numbers and the binary representation. The formalism is used to elucidate the main steps in the derivation: partial evaluation creates propagation functions before carry values are available, finite symbols represent the propagation functions introduced by step 1, and the parallel tree scan algorithm improves the time complexity from O(n) to O(log n). The final result is a precise circuit specification using standard combinational logic gates.</ABSTRACT></RECORD></RECORDS></XML>