Towards provably correct hardware/software partitioning using OCCAM

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