Formal Behavioural Synthesis of Handel-C Parallel Hardware Implementations from Functional Specifications
2014 47th Hawaii International Conference on System Sciences (2003)
Big Island, Hawaii
Jan. 6, 2003 to Jan. 9, 2003
John Hawkins , Centre for Applied Formal Methods South Bank University
Ali E. Abdallah , Centre for Applied Formal Methods South Bank University
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 signifficant 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.
John Hawkins, Ali E. Abdallah, "Formal Behavioural Synthesis of Handel-C Parallel Hardware Implementations from Functional Specifications", 2014 47th Hawaii International Conference on System Sciences, vol. 09, no. , pp. 278a, 2003, doi:10.1109/HICSS.2003.1174808