Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications
Formal behavioural synthesis of Handel-C parallel hardware implementations from functional specifications
复制标题
根据功能规范对 Handel-C 并行硬件实现进行形式化行为综合
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
John Hawkins
中科院分区：
文献类型：
--
作者：
A. Abdallah;John Hawkins
通过利用并行性和硬件实现，可以实现效率的巨大提高。另一方面，用于实现这些改进的常规方法传统上是昂贵的、复杂的并且容易出错。过去十年中的两项重大进展从根本上改变了这些看法。首先是FPGA，它使我们能够通过软件重新配置硬件，大大降低了开发硬件实现的成本。其次，Handel-C语言具有原始的显式并行性，可以将程序编译到FPGA上。在本文中，我们建立在这些最新的技术进步，并提出了一个系统的方法的行为合成。从一个直观的高层次的功能规范的问题，没有注释的并行性，该方法的目的是在Handel-C，随后编译成一个电路上实现可重构硬件推导出一个有效的并行实现。代数定律被系统地用于揭示隐含的并行性，并将规范转换为相互作用的组件的集合。基于数据细化和高阶函数的小型库的形式化方法，然后使用Handel-C中的每个组件来导出行为描述。一个小案例研究说明了这种方法的使用。
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.