Abstract
This paper presents in some detail the systematic derivation of a static bit-level parallel algorithm to implement multiplication of integers, that is to say one which might be implemented as an electronic circuit. The circuit is well known, but the derivation shows that its design can be seen as the consequence of decisions made (and explained) in terms of the abstract algorithm. The systematic derivation serves both as an explanation of the circuit, and as a demonstration that it is correct ‘by construction’. We believe that the technique is applicable to a wide range of similar algorithms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. C. Backhouse, P. J. de Bruin, P. Hoogendijk, G. Malcolm, E. Voermans and J. C. S. P. van der Woude, A relational theory of datatypes, unpublished.
Richard Bird, Ain Introduction to the Theory of Lists, in M. Broy (ed.), Logic of programming and calculi of discrete design, NATO advanced study institutes, Series F: Computer and systems sciences, Springer-Verlag, 1987. pp. 5–42.
Richard Bird, Lectures on constructive functional programming, in M. Broy (ed.), Constructive methods in computing science, NATO advanced study institutes, Series F: Computer and systems sciences, Springer-Verlag, 1989.
D. Borrione and A. Salem, Proving an on-line multiplier with OBJ and TACHE: a practical experience, in [6].
S-K. Chin, Verified synthesis functions for negabinary arithmetic hardware, in [6].
L. J. M. Claesen, Applied formal methods for correct VLSI design, North-Holland, 1989.
Rogardt Heldal, Carsten Kehler Holst, Phil Wadler (eds.), Functional programming, Glasgow 1991, Springer-Verlag (Workshops in Computing), 1992.
Graham Hutton and Ed Voermans, A calculational theory of pers as types, in [7].
Geraint Jones and Mary Sheeran, Relations and Refinement in Circuit Design in Carroll Morgan and J. C. P. Woodcock (eds.), Proceedings of the 3rd Refinement Workshop, 9–11 January 1990, Springer-Verlag (Workshops in Computing), 1991. pp. 133–152.
Geraint Jones and Mary Sheeran, Circuit design in Ruby, in J0rgen Staunstrup (ed.), Formal methods for VLSI design, North-Holland, 1990. pp. 13–70.
Mark B. Josephs, Rudolph H. Mak, Jan Timen Udding, Tom Verhoeff and Jelio T. Yantchev, High-level design of an asynchronous packet routing chip, in [16].
L. G. L. T. Meertens, Constructing a calculus of programs, in J. L. A. van de Snepscheut (ed.), Mathematics of program construction, Springer-Verlag LNCS 375, 1989.
Mary Sheeran, Designing regular array architectures using higher-order functions, in J.-P. Jouannaud (ed.), Functional programming languages and computer architecture, Springer-Verlag LNCS 201, 1985. pp. 220–237.
Mary Sheeran, A note on abstraction in Ruby, in [7].
M. Simonis, Formal verification of multipliers in [6].
Jørgen Staunstrup and R. Sharp (eds.), Designing Correct Circuits, Lyngby 1992, IFIP Transactions A, Volume 5, North-Holland, 1992.
D. Verkest, L. Claesen and H. De Man, A proof of the non-restoring division algorithm and its implementation on the Cathedral-II ALU, in [16].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, G., Sheeran, M. (1993). Designing arithmetic circuits by refinement in Ruby. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds) Mathematics of Program Construction. MPC 1992. Lecture Notes in Computer Science, vol 669. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56625-2_15
Download citation
DOI: https://doi.org/10.1007/3-540-56625-2_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56625-0
Online ISBN: 978-3-540-47613-9
eBook Packages: Springer Book Archive