Abstract
The SPACE machine is introduced as a new type of computer architecture, capable of very fast simulation of highly concurrent systems. The machine is designed to be scalable, constructed from a vast array of boards. The decisions made in the the design of the board are discussed, and the actual hardware (based on an array of Field Programmable Gate Array chips) is described. It is shown that this machine can be programmed by translating a subset of the Occam language into asynchronous modules. Using the Circal process algebra, a new method of formally verifying asynchronous modules for these circuits is presented. This method allows bounded gate delays to be included in a two-level modelling mechanism.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andrew Bailey, George McCaskill, Jim McIntosh, and George Milne. The description and automatic verification of digital circuits in Circal. In P. Camurati and P. Prinetto, editors, Proceeding of the Advanced Research Workshop on Correct Hardware Design Methodologies. Elsevier/North-Holland, 1992. Workshop held from June 12–14, 1991, Turin, Italy.
Andrew Bailey, George A. McCaskill, and George J. Milne. An exercise in the automatic verification of asynchronous designs. Technical Report HDV-26-93, Department of Computer Science, University of Strathclyde, January 1993.
Andrew Bailey and George Milne. Using Circal to analyse Sutherland's asynchronous micropipeline design style. Technical Report HDV-13-91, Department of Computer Science, University of Strathclyde, May 1991.
Erik Brunvand and Robert F. Sproull. Translating concurrent communicating programs into delay-insensitive circuits. Technical Report CMU-CS-89-126, School of Computer Science, Carnegie Mellon University, April 1989.
J. A. Brzozowski and J. C. Ebergen. Recent developments in the design of asynchronous circuits. Technical Report CS-89-18, Computing Science Department, University of Waterloo, May 1989.
J. A. Brzozowski and Jo C. Ebergen. On the delay-sensitivity of gate networks. Computing Science Notes 90/05. Department of Mathematics and Computing Science, Eindhoven University of Technology, June 1990.
J. A. Brzozowski and C-J. Seger. A unified framework for race analysis of asynchronous networks. Journal of the Association of Computing Machinery, 36:20–45, 1989.
J. A. Brzozowski and Michael Yoeli. On a ternary model of gate networks. IEEE Transactions on Computers, 28:178–184, 1979.
Jo C. Ebergen. A formal approach to designing delay-insensitive circuits. Distributed Computing, 5:107–119, 1991.
Jo C. Ebergen. Parallel computations and delay-insensitive circuits. Technical Report CS-91-05, Department of Computer Science, University of Waterloo, January 1991.
Jo C. Ebergen and Sylvain Gingras. An asynchronous stack with constant response time. Submitted to the TALI '92 workshop, 1992.
Jo C. Ebergen and Ad M. G. Peeters. Modulo-n counters: Design and analysis of delay-insensitive circuits. In J. Staunstrup and R. Sharp, editors, Proceedings of the Second IFIP Workshop on Designing Correct Circuits. North-Holland, 1992.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
Inmos. A Tutorial Introduction to occam Programming. BSP Professional Books, 1989.
Tom Kean. Configurable Logic: A Dynamically Programmable Cellular Architecture and its VLSI Implementation. PhD thesis, University of Edinburgh, Dec 1989.
Alain J. Martin. Compiling communicating processes into delay-insensitive VLSI circuits. Distributed Computing, 1:226–234, 1986.
George McCaskill. The XCircal user guide and reference manual. Technical Report HDV-18-91, Department of Computer Science, University of Strathclyde, October 1991.
George J. Milne. Circal and the representation of communication, concurrency and time. Association of Computing Machinery Transactions on Programming Languages and Systems, 7(2), 1985.
George J. Milne. The formal description and verification of hardware timing. IEEE Transactions on Computers, 40(7), 1991.
Ivan E. Sutherland. Micropipelines. Communications of the Association of Computing Machinery, 32(6):720–738, June 1989.
Kees van Berkel, Joep Kessels, Marly Roncken, Ronald Saeijs, and Frits Schalij. The VLSI-programming language Tangram and its translation into handshake circuits. In The European Design and Automation Conference, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shaw, P., Milne, G. (1993). A highly parallel FPGA-based machine and its formal verification. In: Grünbacher, H., Hartenstein, R.W. (eds) Field-Programmable Gate Arrays: Architecture and Tools for Rapid Prototyping. FPL 1992. Lecture Notes in Computer Science, vol 705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57091-8_41
Download citation
DOI: https://doi.org/10.1007/3-540-57091-8_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57091-2
Online ISBN: 978-3-540-47902-4
eBook Packages: Springer Book Archive