Title :
Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications
Author :
Abdallah, Ali E. ; Hawkins, John
Author_Institution :
Centre for Appl. Formal Methods, South Bank Univ., London, UK
Abstract :
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.
Keywords :
field programmable gate arrays; formal specification; functional programming; high level synthesis; parallel architectures; parallel programming; reconfigurable architectures; FPGA; Handel-C language; Handel-C parallel hardware implementations; algebraic laws; component behavioural description; data refinement; formal behavioural synthesis; formal methods; hardware parallelism; hardware reconfiguration; high level functional specification; interacting components; program compiling; Algorithm design and analysis; Application software; Art; Circuit synthesis; Costs; Field programmable gate arrays; Functional programming; Hardware; High level languages; Programming profession;
Conference_Titel :
System Sciences, 2003. Proceedings of the 36th Annual Hawaii International Conference on
Print_ISBN :
0-7695-1874-5
DOI :
10.1109/HICSS.2003.1174808