As mentioned in our previous Progress Report, our formal approach to hardware/software partitioning uses occam both as the input and the output language of the partitioning process. Using occam it is possible to regard hardware/software partitioning as an application of program transformation. The algebraic laws of occam can be used to transform an arbitrary source program (the input) into a program whose structure reflects the software and hardware components, and how they interact to achieve the overall goal. It is possible to express this in occam because it includes features to express parallelism and communication.
Our approach has been structured into four four major phases: splitting, classification, clustering and joining. The purpose of the splitting is to break the original input into a set of very simple parallel processes, in order to allow the other phases to carry out a flexible analysis of the design space. A normal form to express the output of the spliting has been formally defined and the necessary reduction theorems have been stated and proved.
The form in which the result of the splitting is expressed allows great flexibility during the classification and clustering phases, since every permutation of the simple processes can be considered as a potential candidate to form a suitable cluster. The phases of classification and clustering are specific of the particular partitioning algorithm on which we have based our approach, and are the responsibility of another researcher, Dr. Edna Barros, through another KIT Project (KIT 128). These phases are concerned with the efficiency of the partitioned program; they have nothing to do with the correctness of the process. One important contribution of our approach to partitioning is the separation between correctness and efficiency concerns.
An important result obtained by the grant was an innovative approach to hardware/software codesign (and in particular to partitioning): a formal characterisation of the entire process as an algebraic transformation task in such a way that correctness is guaranteed by construction. A more practical result was the integration of this work on partitioning with the Oxford approach to codesign. A preliminary strategy has been defined to allow the output of the partitioning process to be direct implemented in the HARP2 Board, a codesign architecture developed jointly by Oxford University Computing Laboratory and Sundance Multiprocessor Technology Ltd.
In addition, this strategy has been partially implemented as an extension of the Occam Transformation System, originally developed at Oxford. This is based on the functional language SML. The splitting and the joining phases are coded as functions which carry out the necessary transformations. The classification and clustering have been implemented in the C language, for efficiency purposes. An important aspect of the implementation is that it reflects the separation of concerns described previously: for splitting and joining we have built an environment based on transformations, whereas for classification and clustering the emphasis is on efficiency.