Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications

Enormous improvements in efficiency can be achieved through exploiting parallelism and realizing implementation in hardware. On the other hand, conventional methods for achieving these improvements are traditionally costly, complex and error prone. Two significant advances in the past decade have radically changed these perceptions. Firstly, the FPGA, which gives us the ability to reconfigure hardware through software, dramatically reducing the costs of developing hardware implementations. Secondly, the language Handel-C with primitive explicit parallelism which can compile programs down to an FPGA. In this paper, we build on these recent technological advances and present a systematic approach of behavioural synthesis. Starting with an intuitive high level functional specification of a problem, given without annotation of parallelism, the approach aims at deriving an efficient parallel implementation in Handel-C, which is subsequently compiled into a circuit implemented on reconfigurable hardware. Algebraic laws are systematically used for exposing implicit parallelism and transforming the specification into a collection of interacting components. Formal methods based on data refinement and a small library of higher order functions are then used to derive behavioural description in Handel-C of each component. A small case study illustrates the use of this approach.