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

Abdallah, A. E. and Hawkins, J. (2003) Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications. In: System Sciences, 2003. Proceedings of the 36th Annual International Conference. IEEE Conference Publications, pp. 1-11. ISBN 0-7695-1874-5

Full text not available from this repository. (Request a copy)

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.

Item Type: Book Section
Uncontrolled Keywords: Hardware, Field programmable gate arrays, Costs, Algorithm design and analysis, Circuit synthesis, Application software, High level languages, Programming profession, Art, Functional programming ,data refinement, formal behavioural synthesis, Handel-C parallel hardware implementations, hardware parallelism, FPGA, hardware reconfiguration, Handel-C language, program compiling, high level functional specification, interacting components, formal methods, component behavioural description, algebraic laws
Subjects: G400 Computer Science
Divisions: Faculty of Computing, Engineering and the Built Environment
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology > Cyber Security
UoA Collections > UoA11: Computer Science and Informatics
Depositing User: Oana-Andreea Dumitrascu
Date Deposited: 07 Apr 2017 10:27
Last Modified: 07 Apr 2017 10:27
URI: http://www.open-access.bcu.ac.uk/id/eprint/4221

Actions (login required)

View Item View Item

Research

In this section...