Subject Committee: Software Engineering

Technology area: Formal Computer Science

Grant title: Provably Correct Hardware/Software Co-design

Principal investigator: Prof C.A.R. Hoare

Co-investigator/other participants: J.P. Bowen

Institution: Oxford University

Department name & address: Computing Laboratory
Wolfson Building, Parks Road, OXFORD OX1 3QD, UK

Objectives

1. To ensure maximum UK industrial benefit from the ESPRIT Basic Research ProCoS project.
2. Develop a prototype hardware/software compiler for embedded ASIC applications.
3. Contribute to European collaboration.

Progress/deliverables

• J.P. Bowen and He Jifeng, Programs to Hardware. In P.G. Larsen (ed.), Tutorial Material, Formal Methods Europe '93, Industrial-Strength Formal Methods, Odense, Denmark, pages 437-450, 1993. In A.P. Ravn (ed.), Provably Correct Systems (ProCoS) tutorial.
• He Jifeng, I. Page and J.P. Bowen, Towards a provably correct hardware implementation of Occam. In G.J Milne and L. Pierre (eds.), Correct Hardware Design and Verification Methods, Proc. IFIP WG10.2 Advanced Research Working Conference, CHARME'93, Springer-Verlag, Lecture Notes in Computer Science, 683, pages 214-225, 1993.
• J.P. Bowen, M. Fränzle, E.-R. Olderog and A.P. Ravn, Developing Correct Systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland, IEEE Computer Society Press, pages 176-187, 1993.
• J.P. Bowen et al., A ProCoS II Project Description: ESPRIT Basic Research Project 7071. Bulletin of the European Association for Theoretical Computer Science (EATCS), volume 50, pages 128-137, June 1993. Also available in on-line hypertext form.
• J.P. Bowen et al., A ProCoS-WG Working Group Description: ESPRIT Basic Research 8694. Bulletin of the European Association for Theoretical Computer Science (EATCS), 53, pages 136-145, June 1994. Also available in on-line hypertext form.
• J.P. Bowen, He Jifeng and I. Page, Hardware Compilation. In J.P. Bowen (ed.), Towards Verified Systems, Elsevier Science B.V., Real-Time Safety Critical Systems series, volume 2, chapter 10, pp 193-207, 1994.
• I. Page, Constructing Hardware-Software Systems Reliably. IEE colloquium, May 1994.
• C.A.R. Hoare and I. Page, Hardware and Software: Closing the Gap. Transputer Communications, 2(2):69-90, June 1994.
• C.A.R. Hoare, Mathematical Models for Computing Science. Notes, Oxford University Computing Laboratory, August 1994. (65 pages)
  Also available using PostScript fonts if preferred.
• He Jifeng and J.P. Bowen, Specification, Verification and Prototyping of an Optimized Compiler. Formal Aspects of Computing, 6(6), pp 643-658, 1994.
• J.P. Bowen, Rapid Compiler Implementation. Chapter 10 in He Jifeng, Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers, McGraw-Hill International Series in Software Engineering, pp 141-169, 1995.

Future plans/exploitation

• The Hardware Compilation Group at OUCL including information on provably correct hardware compilation.

• ESPRIT Basic Research COBRA Project (8135) on hardware/software co-design.

• Cornell co-design tool (see Cornell index) which compiles Promela (a CSP-like language) to C++ and VHDL.

• ESPRIT NADA project on new hardware design methods including the hardware/software interface.

• 6th IEEE International Workshop Rapid Systems Prototyping, Chapel Hill, North Carolina, USA, 7-9 June 1995.

• Ruby - a notation and design discipline for the development of regular integrated circuits and similar hardware and software architectures.

• ACID - automation of circuit design, including hardware/software integration.

• The Design Group, Department of Computer Science, Technical University of Denmark. See 1995 Summer School on Hardware/Software Codesign.

• CODES/CASHE '96, 4th International Workshop on Hardware/Software Co-Design, Pittsburgh, Pennsylvania, USA, 18-20 March 1996.

• ECBS '96, 9th International Symposium and Workshop on Engineering of Computer Based Systems, Graf-Zeppelin-Haus Conference Center, Friedrichshafen, Germany, 11-15 March 1996. Includes co-design.

• IFIP Working Conference on Hardware/Software Codesign, Zakopane, Poland, 29-31 August 1996.

• IMEC Symposium on Hardware/Software Co-design, organised by OMI-IUN-2 in co-operation with DSP Valley, Belgium, 18-20 February 1997.

• VHDL-93 parser (and formatter) written in SWI-Prolog and Quintus Prolog.

• EPSRC guidance.

• ESPRIT III INSYDE project (Integrated Methods for Evolving System Design) on methodology for software/hardware design, and the Special Interest Group for Hybrid Systems Design, School of Computer Applications, Dublin City University, Ireland.

• VHDL International Users' Forum (VIUF).

• Compositional Methods for Hardware/Software Co-Design EPSRC project, starting 1998.