Skip to main content
SpringerLink
Log in
Book cover

Transactions on Computational Science I pp 1–36Cite as

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

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((TCOMPUTATSCIE,volume 4750))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. Bailey, B., Gajski, D.: RTL Semantics and Methodology. In: 14th International Symposium on Systems Synthesis (ISSS), Montreal, Canada, pp. 69–74 (2001)

    Google Scholar 

  3. Black, D.C., Donovan, J.: SystemC: From the Ground Up, 1st edn., p. 244. Springer, Heidelberg (2004)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC, 1st edn., p. 240. Springer, Heidelberg (2002)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. 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)

    Google Scholar 

  15. R. Hartenstein. Handbook of Nature-Inspired and Innovative Computing. Integrating Classical Models with Emerging Technologies, chapter Morphware and Configware. p. 780, Springer, Heidelberg (2005)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Hinchey, M.G., Bowen, J.P.: Industrial-Strength Formal Methods in Practice. In: Formal Approaches to Computing and Information Technology (FACIT), Springer, London (1999)

    Google Scholar 

  19. 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)

    Article  MATH  Google Scholar 

  20. Hughes, J., Jacobs, B.: Simulations in Coalgebra. Theoretical Computer Science 327(1-2), 71–108 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction. Bulletin of EATCS 62, 222–259 (1997)

    MATH  Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. 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)

    Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Rutten, J.J.M.M.: Universal Coalgebra: A Theory of Systems. Theoretical Computer Science 249(1), 3–80 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  27. Rutten, J.J.M.M.: Elements of Stream Calculus (An Extensive Exercise in Coinduction). Electronic Notes in Theoretical Computer Science, 45 (2001)

    Google Scholar 

  28. 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)

    Google Scholar 

  29. Rutten, J.J.M.M.: Algebra, Bitstreams, and Circuits. Technical Report SEN-R0502, CWI, Amsterdam, The Netherlands (2005)

    Google Scholar 

  30. 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)

    Google Scholar 

  31. 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)

    Google Scholar 

  32. Tessier, R., Burleson, W.: Reconfigurable Computing for Digital Signal Processing: A Survey. VLSI Signal Processing 28(1–2), 7–27 (2001)

    Article  MATH  Google Scholar 

  33. 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)

    Google Scholar 

  34. 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)

    Google Scholar 

  35. 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)

    Google Scholar 

  36. 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)

    Chapter  Google Scholar 

  37. 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)

    Article  Google Scholar 

  38. 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)

    Chapter  Google Scholar 

  39. 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)

    Chapter  Google Scholar 

  40. Woodcock, J.C.P.: First Steps in the Verified Software Grand Challenge. IEEE Computer 39(10), 57–64 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Applied Formal Methods, Institute for Computing Research Faculty of BCIM, London South Bank University, Borough Road, London, SE1 0AA, UK

    Phan Cong Vinh & Jonathan P. Bowen

Authors
  1. Phan Cong Vinh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan P. Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marina L. Gavrilova C. J. Kenneth Tan

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation