Correct compilation of specifications to deterministic asynchronous circuits
- 241 Downloads
We have shown that Martin et al.'s methodology can be made more rigorous. In order to accomplish this the new concepts of partial declarations, module and component, mutual exclusion violations, fairness, handshaking variables, distinguished ports, equational rewriting, separate compilation and observable determinism were introduced.
Two recent papers address the same general problem of proving correctness of asynchronous circuit compilation [WBB92, vB92]. These two systems are more closely related to each other than either are to our work. In brief, the main advantage over our work is lack of the mutual exclusion issue and complications introduced thereby, and the disadvantages are expressiveness of the specification language and speed of resulting circuits.
In a prelimary report [WBB92], Weber, Bloom, and Brown define a process language Joy and its compilation to asynchronous circuitry. Joy has a number of syntactic restrictions including the restriction that no processes may share variables or passive port names. Their correctness proof is based on a bisimulation equivalence, which does not incorporate fairness.
van Berkel gives a correctness proof for compiling the CSP-based specification language Tangram to circuits. Tangram can only have single uses of each port, and disallows concurrent reads. His proof of correctness is based on a trace equivalence that does not take fairness into account.
- [BM88]Steven M. Burns and Alain J. Martin. Synthesis of self-timed circuits by program transfomation. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, pages 99–116. Elsevier Science Publishers B.V. (North-Holland), 1988.Google Scholar
- [BS89]Erik Brunvand and Robert F. Sproull. Translating concurrent programs into delay-insensitive circuits. In Proceedings of ICCAD-89, pages 262–265. IEEE Computer Society Press, 1989.Google Scholar
- [Hen88]M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.Google Scholar
- [Hoa85]C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
- [Mar90]Alain J. Martin. Programming in VLSI: From communicating processes to delay-insensitive circuits. In C. A. R. Hoare, editor, Developments in Concurrency and Communication. Addison-Wesley, 1990. UT Year of Programming Institute on Concurrent Programming.Google Scholar
- [MBL+89]Alain J. Martin, Steven M. Burns, T.K. Lee, Drazen Borkovic, and Pieter J. Hazewindus. The design of an asynchronous microprocessor. In Charles L. Seitz, editor, Advanced Research in VLSI: Proc. of the Decennial Caltech Conference on VLSI, pages 351–373, 1989.Google Scholar
- [MBM89]Teresa H.-Y. Meng, Robert W. Brodersen, and David G. Messerschmitt. Automatic synthesis of asynchronous circuits from high-level specifications. IEEE Trans. on CAD, 8(ll):1185–1205, November 1989.Google Scholar
- [SZ92]Scott F. Smith and Amy E. Zwarico. Provably correct synthesis of asynchronous circuits. In Jørgen Staunstrup and Robin Sharp, editors, 2nd Workshop on Designing Correct Circuits, Lyngby, pages 237–260. Elsevier, North Holland, 1992.Google Scholar
- [SZ93]Scott F. Smith and Amy E. Zwarico. Correct compilation of specifications to deterministic asynchronous circuits. Technical Report 05–93, The Johns Hopkins University, Department of Computer Science, Baltimore, MD 21218 USA., 1993. Anonymous ftp: ftp.cs.jhu.edu.Google Scholar
- [vB92]Kees van Berkel. Handshake Circuits: an intermediary between communicating processes and VLSI. PhD thesis, Eindhoven U., May 1992. Oxford University Press, to appear.Google Scholar
- [WBB92]S. Weber, B. Bloom, and G. Brown. Compiling Joy to silicon. In Advanced research in VLSI and parallel systems: proceedings of the 1992 Brown/MIT conference. MIT Press, 1992.Google Scholar