Formalization of Data Flow Computing and a Coinductive Approach to Verifying Flowware Synthesis

Reconfigurable computing refers to the notions of configware and flowware. Configware means structural programming, or programming in space to execute computation in space. Flowware means data-flow programming that schedules the data flow for output from or input to the configware architecture. In this paper, data flows of a synthesized computation are formalized. This means that data flow is specified as a behavioral stream function in stream calculus, which is used to underpin the semantics for Register Transfer Level (RTL) synthesis. A stream representation allows the use of coinductive principles in stream calculus. In particular, using the coinductive proof principle, we show that behavioral stream functions in the three-stage synthesis process (scheduling, register allocation and binding, allocation and binding of functional units) are always bisimilar regardless of changes in a scheduling, allocation or binding procedure. Our formalization makes pipelining possible, in which all functional units as well as registers of hardware resources are reused during different control steps (C-steps). Moreover, a coinductive approach to verifying flowware synthesis, which is independent of the heuristic during register allocating and binding step, is proposed as a practical technique.

Keywords: Dynamic reconfiguration; Reconfigurable computing; Dynamically Programmable Field Array (DPGA); Flowware; Configware; Configware engineering; Embedded systems; Formal methods

By Phan Cong-Vinh
Paper title: Formalization of Data Flow Computing and a Coinductive Approach to Verifying Flowware Synthesis.
Journal title: LNCS Transactions of Computational Science I.
Vol. 4750, No. 1, pp: 1-36, 2008.
Publisher: Springer-Verlag