Computing at Glasgow University
Paper ID: 7069
DCS Tech Report Number: TR-1995-19

A formal derivation of a parallel binary addition circuit
O'Donnell,J.T. Ruenger,G.

Publication Type: Tech Report (internal)
Appeared in: DCS Tech Report
Page Numbers :
Publisher: University of Glasgow
Year: 1995

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.

Keywords: carry lookahead adder, formal derivation, hardware description language

Bibtex entry Endnote XML