Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ast, A., Becker, J., Hartenstein, R., Kress, R., Reinig, H., Schmidt, K.: Data- Procedural Languages for FPL-based Machines. In: Hartenstein, R.W., Servít, M.Z. (eds.) FPL 1994. LNCS, vol. 849, pp. 183–195. Springer, Heidelberg (1994)
Bailey, B., Gajski, D.: RTL Semantics and Methodology. In: 14th International Symposium on Systems Synthesis (ISSS), Montreal, Canada, pp. 69–74 (2001)
Black, D.C., Donovan, J.: SystemC: From the Ground Up, 1st edn., p. 244. Springer, Heidelberg (2004)
Bowen, J.P., Hinchey, M.G.: Formal Methods. In: Tucker Jr., A.B. (ed.) Computer Science Handbook, ch.106, Section XI, Software Engineering, 2nd edn., pp. 106–1 – 106–125. Chapman & Hall / CRC, ACM, USA (2004)
DeHon, A.: DPGA Utilization and Application. In: 4th International Symposium on Field Programmable Gate Arrays (FPGA 1996), Monterey, CA, US, 11–13 February 1996, pp. 115–121. ACM Press, New York (1996)
DeHon, A., Wawrzynek, J.: Reconfigurable Computing: What, Why, and Implications for Design Automation. In: 36th Design Automation Conference (DAC), New Orleans, LA, USA, 21–25 June 1999, pp. 610–615. ACM Press, New York (1999)
Eisenbiegler, D., Kumar, R.: Formally Embedding Existing High Level Synthesis Algorithms. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 2–4. Springer, Heidelberg (1995)
Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC, 1st edn., p. 240. Springer, Heidelberg (2002)
Hartenstein, R.: The Microprocessor is No Longer General Purpose: Why Future Reconfigurable Platforms Will Win. In: 2nd Annual International Conference on Innovative Systems in Silicon, Austin, TX, USA, 8–10 October 1997, pp. 2–12. IEEE, Los Alamitos (1997)
Hartenstein, R.: A Decade of Reconfigurable Computing: A Visionary Retrospective. In: Design, Automation, and Test in Europe Conference (DATE), Munich, Germany, 13–16 March 2001, pp. 642–649. IEEE, Los Alamitos (2001)
Hartenstein, R.: Coarse Grain Reconfigurable Architectures. In: Asia and South Pacific Design Automation Conference (ASP-DAC), Yokohama, Japan, 30 January – 2 February 2001, pp. 564–569. IEEE, Los Alamitos (2001)
Hartenstein, R.: Reconfigurable Computing: A New Business Model and its Impact on SoC Design. In: Euromicro Symposium on Digital Systems, Design (DSD), Warzaw, Poland, 4–6 September 2001, pp. 103–110. IEEE, Los Alamitos (2001)
Hartenstein, R.: Trends in Reconfigurable Logic and Reconfigurable Computing. In: 9th International Conference on Electronics, Circuits and Systems (ICECS), Dubrovnik, Croatia, 15–18 September 2002, vol. 2, pp. 801–808. IEEE, Los Alamitos (2002)
Hartenstein, R.: Are We Really Ready for the Breakthrough? [morphware]. In: International Parallel and Distributed Processing Symposium (IPDPS), Nice, France, 22–26 April 2003, IEEE, Los Alamitos (2003) (CD-ROM)
R. Hartenstein. Handbook of Nature-Inspired and Innovative Computing. Integrating Classical Models with Emerging Technologies, chapter Morphware and Configware. p. 780, Springer, Heidelberg (2005)
Hartenstein, R., Kress, R.: A Datapath Synthesis System for the Reconfigurable Datapath Architecture. In: Design Automation Conference of the ASP-DAC 1995/CHDL 1995/VLSI 1995, IFIP International Conference on Hardware Description Languages, IFIP International Conference on Very Large Scale Integration, Asian and South Pacific, Chiba, Japan, 29 August – 1 September 1995, pp. 479–484. IEEE, Los Alamitos (1995)
Herz, M., Hartenstein, R., Miranda, M., Brockmeyer, E., Catthoor, F.: Memory Addressing Organization for Stream-based Reconfigurable Computing. In: 9th International Conference on Electronics, Circuits and Systems (ICECS), Dubrovnik, Croatia, 15–18 September 2002, vol. 2, pp. 813–817. IEEE, Los Alamitos (2002)
Hinchey, M.G., Bowen, J.P.: Industrial-Strength Formal Methods in Practice. In: Formal Approaches to Computing and Information Technology (FACIT), Springer, London (1999)
Hoare, C.A.R., Hayes, I.J., Jifeng, H., Morgan, C.C., Roscoe, A.W., Sanders, J.W., Sorensen, I.H., Spivey, J.M., Sufrin, B.A.: Laws of Programming. Communications of the ACM 30(8), 672–686 (1987)
Hughes, J., Jacobs, B.: Simulations in Coalgebra. Theoretical Computer Science 327(1-2), 71–108 (2004)
Jacobs, B.: Exercises in Coalgebraic Specification. In: Blackhouse, R., Crole, R.L., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 237–280. Springer, Heidelberg (2002)
Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction. Bulletin of EATCS 62, 222–259 (1997)
Kumar, R., Blumenröhr, C., Eisenbiegler, D., Schmid, D.: Formal Synthesis in Circuit Design – A Classification and Survey. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 6–8. Springer, Heidelberg (1996)
Lysaght, P.: Aspects of Dynamically Reconfigurable Logic. In: Colloquium on Reconfigurable Systems, Glasgow, Scotland, UK, 10 March 1999, vol. 61, pp. 1/1–1/5. IEE (1999)
Rutten, J.J.M.M.: Automata and Coinduction (an Exercise in Coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 8–11. Springer, Heidelberg (1998)
Rutten, J.J.M.M.: Universal Coalgebra: A Theory of Systems. Theoretical Computer Science 249(1), 3–80 (2000)
Rutten, J.J.M.M.: Elements of Stream Calculus (An Extensive Exercise in Coinduction). Electronic Notes in Theoretical Computer Science, 45 (2001)
Rutten, J.J.M.M.: An Application of Stream Calculus to Signal Flow Graphs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 4–7. Springer, Heidelberg (2004)
Rutten, J.J.M.M.: Algebra, Bitstreams, and Circuits. Technical Report SEN-R0502, CWI, Amsterdam, The Netherlands (2005)
Rutten, J.J.M.M.: Algebraic Specification and Coalgebraic Synthesis of Mealy Automata. In: Barbosa, L.S., Liu, Z. (eds.) 2nd International Workshop on Formal Aspects of Component Software (FACS), 24–25 October 2005, vol. 160, pp. 305–319. Elsevier Science Publishers Ltd, UNU/IIST, Macao (2006)
Sangiorgi, D.: Bisimulation: From the Origins to Today. In: 19th Annual Symposium on Logic in Computer Science, Turku, Finland, 13–17 July 2004, pp. 13–17. IEEE, Los Alamitos (2004)
Tessier, R., Burleson, W.: Reconfigurable Computing for Digital Signal Processing: A Survey. VLSI Signal Processing 28(1–2), 7–27 (2001)
Vinh, P.C.: Formal Aspects of Dynamic Reconfigurability in Reconfigurable Computing Systems. PhD thesis, London South Bank University, 103 Borough Road, London SE1 0AA, UK (May 4, 2006)
Vinh, P.C., Bowen, J.P.: Formalising Configuration Relocation Behaviours for Reconfigurable Computing. In: SFP Workshop, FDL 2002: Forum on Specification & Design Languages, Marseille, France, September 24–27, 2002 (2002) (CD-ROM)
Vinh, P.C., Bowen, J.P.: An Algorithmic Approach by Heuristics to Dynamical Reconfiguration of Logic Resources on Reconfigurable FPGAs. In: 12th International Symposium on Field Programmable Gate Arrays, Monterey, CA, USA, 22–24 February 2004, p. 254. ACM/SIGDA (2004)
Vinh, P.C., Bowen, J.P.: A Provable Algorithm for Reconfiguration in Embedded Reconfigurable Computing. In: Hinchey, M.G. (ed.) 29th Annual IEEE/NASA Software Engineering Workshop (SEW), Greenbelt, MD, USA, 6–7 April 2005, pp. 245–252. IEEE Computer Society Press, Los Alamitos (2005)
Vinh, P.C., Bowen, J.P.: Continuity Aspects of Embedded Reconfigurable Computing. Innovations in Systems and Software Engineering: A NASA journal 1(1), 41–53 (2005)
Vinh, P.C., Bowen, J.P.: POM Based Semantics of RTL and a Validation Method for the Synthesis Results in Dynamically Reconfigurable Computing Systems. In: Rozenblit, J., O’Neill, T., Peng, J. (eds.) 12th Annual International Conference and Workshop on the Engineering of Computer Based Systems (ECBS), Greenbelt, MD, USA, 4–5 April 2005, pp. 247–254. IEEE Computer Society Press, Los Alamitos (2005)
Vinh, P.C., Bowen, J.P.: A Formal Approach to Aspect-Oriented Modular Reconfigurable Computing. In: 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE), Shanghai, China, 6–8 June 2007, pp. 369–378. IEEE Computer Society Press, Los Alamitos (2007)
Woodcock, J.C.P.: First Steps in the Verified Software Grand Challenge. IEEE Computer 39(10), 57–64 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Vinh, P.C., Bowen, J.P. (2008). Formalization of Data Flow Computing and a Coinductive Approach to Verifying Flowware Synthesis . In: Gavrilova, M.L., Tan, C.J.K. (eds) Transactions on Computational Science I. Lecture Notes in Computer Science, vol 4750. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79299-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-79299-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79298-7
Online ISBN: 978-3-540-79299-4
eBook Packages: Computer ScienceComputer Science (R0)