Hardware Compilation

The well-understood algebraic semantics of Occam (itself based on CSP) are taken as the basis of a compilation strategy. The use of Occam has allowed the compilation process to be specified as a series of correctness-preserving transformations on the user program resulting in a normal-form program. A prototype version of the compiler has been implemented in Prolog, which means that the compilation process is itself the necessary proof of correctness.

Extensive general on-line information on Provably Correct Systems is available.

Publications

A number of hardware compilation papers relevant to Provably Correct Systems are available on-line. The issue of producing Provably Correct Systems has been an important aspect of the research into hardware compilation at the OUCL:

Towards a Provably Correct Hardware Implementation of Occam, He Jifeng, Ian Page and Jonathan Bowen. In G.J. Milne and L. Pierre (eds.), Correct Hardware Design and Verification Methods, Proc. IFIP WG10.2 Advanced Research Working Conference, CHARME '93, Arles, France, 24-26 May 1993, Springer-Verlag, LNCS 683, pp 214-225, 1993.
Hardware Compilation, Jonathan Bowen, He Jifeng and Ian Page. In J.P. Bowen (ed.), Towards Verified Systems, Elsevier Science Publishers, Real-Time Safety Critical Systems series, volume 2, chapter 10, pp 193-207, 1994.
Simulation Approach to Provably Correct Hardware Compilation, He Jifeng and Zheng Jianping. In H. Langmaack, W.-P. de Roever and J. Vytopil, Formal Techniques in Real Time and Fault Tolerant Systems, Springer-Verlag, LNCS 863, pp 336-350, 1994.

The ProCoS II project has been investigating the development of computer-based systems at levels of abstraction from requirement down to digital hardware. The following papers present the approach of the project, including provably correct hardware compilation:

Developing Correct Systems, Jonathan Bowen, Martin Fränzle (Christian-Albrechts Universität zu Kiel, Germany), Ernst-Rüdiger Olderog (Universität Oldenburg, Germany), Anders P. Ravn (Technical University of Denmark). Invited special presentation. Proc. Fifth Euromicro Workshop on Real-Time Systems, IEEE Computer Society Press, pp 176-187, 1993.
Provably Correct Systems, He Jifeng, C.A.R. Hoare, Martin Fränzle, Markus Müller-Ulm Ernst-Rüdiger Olderog, Michael Schenke, Anders P. Ravn and Hans Rischel. In H. Langmaack, W.-P. de Roever and J. Vytopil, Formal Techniques in Real Time and Fault Tolerant Systems, Springer-Verlag, LNCS 863, pp 288-335, 1994. (48 pages)
Provably Correct Systems - FTRTFT'94 Tutorial, Jonathan Bowen, C.A.R. Hoare, Michael R. Hansen, Anders P. Ravn, Ernst-Rüdiger Olderog, Michael Schenke, Martin Fränzle, Markus Müller-Ulm He Jifeng and Zheng Jianping. Third International School and Symposium, Formal Techniques in Real Time and Fault Tolerant Systems, 19-23 September 1994, Lübeck, Germany: School Material. Christian-Albrechts-Universität, 1994. (100 pages)

Other Information

Local links:

Provably Correct Hardware/Software Co-design EPSRC project.
ESPRIT/NSF ProCoS-US initiative on Provably Correct Hardware Compilation with Cornell University, USA.
Hardware compilation publications in the ESPRIT ProCoS II project bibliography.
Hardware Compilation and Provably Correct Systems Groups Seminar Series, OUCL, Oxford, UK.

Remote links:

Related commercial Handel-C compiler marketed by Embedded Solutions Ltd. This has a C-like syntax but an Occam-like semantics. The netlists produced by the compiler are targetted at Xilinx Field Programmable Gate Arrays (FPGAs), and are considerable more optimized, but the compiling scheme has not been verified.
FPGA research, University of Toronto, Canada.

Last updated by Jonathan Bowen, 18 September 1998.
Comments, information suitable for inclusion and pointers to relevant on-line papers are welcome.

Part of the OUCL hardware compilation archive.