Abstract
We describe work completed on a custom SECD chip which is powerful enough to run a LispKit compiler. The 20,000 transistor design was fabricated in 1988 and is being interfaced to a workstation so that it can run downloaded programs. We discuss the evolution of the architecture from its abstract specification and abstraction issues that arose at key levels in the verification of the design. The verification is being undertaken in Cambridge HOL. One hard issue (garbage collection) has been left over for a second iteration of the specification and verification.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Burge. Recursive programming techniques. Addison-Wesley, New York, 1975.
A. J. Field and P. G. Harrison. Functional programming. Addison-Wesley, New York, 1988.
M. J. Hermann, G. Birtwistle, B. Graham, and T. Simpson. The architecture of Henderson's SECD machine. Research Report 89/340/02, Computer Science Department, University of Calgary, 1989.
P. Henderson. Functional programming; applications and implementation. Prentice Hall, London, 1980.
I. A. Mason. The Semantics of Destructive Lisp. Center for the Study of Language and Information, Stanford, 1986.
I. A. Mason. Verification of Programs that Destructively Manipulate Data. Science of Computer Programming, 10:177–210, 1988.
T. F. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 267–291, Norwell, Massachusetts, 1988. Kluwer.
G. D. Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1(1):125–159, 1975.
T. Simpson, G. Birtwistle, B. Graham, and M. J. Hermann. A compiler for LispKit targetted at Henderson's SECD machine. Research Report 89/339/01, Computer Science Department, University of Calgary, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graham, B., Birtwistle, G. (1990). Formalising the design of an SECD chip. In: Leeser, M., Brown, G. (eds) Hardware Specification, Verification and Synthesis: Mathematical Aspects. Lecture Notes in Computer Science, vol 408. Springer, New York, NY. https://doi.org/10.1007/0-387-97226-9_23
Download citation
DOI: https://doi.org/10.1007/0-387-97226-9_23
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97226-8
Online ISBN: 978-0-387-34801-8
eBook Packages: Springer Book Archive