Towards provably correct hardware/software partitioning using occam

ABSTRACT

In this paper we present some ideas towards an approach to provably correct hardware/software partitioning. We use occam as the source programming language and perform the partitioning by applying a series of algebraic transformations on the source program. The result is still an occam program; its structure reflects the hardware and software components, and how they interact to achieve the overall goal. A simple case study is developed to illustrate the partitioning and to show how the transformations can be proved to preserve an algebraic semantics of occam.

REFERENCES

• 1: E. Barros. Hardware/Software Partitioning using UNITY. PhD thesis, Universität Tübingen, 1993.
• 2: E. Barros, X. Xiong, and W. Rosentiel. Hardware/Software Partitioning with UNITY. In Handouts of International Workshop on Hardware-Software Co-design, 1993.
• 3: R. Ernst and J. Henkel. Hardware-Software Codesign of Embedded Controllers Based on Hardware Extraction. In Handouts of the International Workshop on Hardware-Software Co-Design, October 1992.
• 4: G. C. Fox, Solving problems on concurrent processors, Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 5: J. Goguen et al. Introducing obj. Technical report, SRI International, 1993. To appear.
• 6: M. Goldsmith. The oxford occam transformation system. Technical report, Oxford University Computing Laboratory, January 1988.
• 7: R. Gupta and G. De Micheli. System-level Synthesis Using Re-programmable Components. In Proceedings of EDAC, pages 2--7, 1992.
• 8: Jifeng He, I. Page, and J. Bowen. A provably correct hardware implementation of occam. Technical report, ProCoS Project Document {OU HJF 9/5}, Oxford University Computing Laboratory, November 1992.
• 9: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 10: C. A. R. Hoare , He Jifeng , A. Sampaio, Normal form approach to compiler design, Acta Informatica, v.30 n.9, p.701-739, Nov. 1993
• 11: A. W. Roscoe , C. A. R. Hoare, The laws of Occam programming, Theoretical Computer Science, v.60 n.2, p.177-229, September 1988 [doi>10.1016/0304-3975(88)90049-7]
• 12: A. Sampaio. An Algebraic Approach to Compiler Design. PhD thesis, Oxford University Computing Laboratory, 1993.