Skip to main content
SpringerLink
Log in

Formal Design Flows for Embedded IoT Hardware

  • Chapter
  • First Online:
Components and Services for IoT Platforms

  • 3141 Accesses

Abstract

Taking into account the current complexity of IoT devices and hardware/software modules, there is a need to shorten the design time of embedded systems along with their custom hardware blocks. Already many microcontroller vendors include embedded hardware security blocks into their products so as to prohibit the potential security attackers and threats. Moreover, when the hardware design tools and methods are based on formal and rapid techniques, then product-to-market delays are eliminated. This chapter discusses a novel high-level synthesis technique which is rapid, and is based on formal methodologies. This synthesis-based methodology is used for the rapid and formal development of custom hardware blocks that collaborate with their host environment to deliver complete IoT nodes. Due to the formal nature of the logic programming-based synthesis transformations of the design tools, the produced hardware is provably correct in respect with the given executable specifications in high-level program code. Moreover, the automatically generated verification testbenches from exactly the same synthesis design model make the verification unified, formal, and rapid. The discussed synthesis and verification approach is rapid, flexible, formal and includes a number of input and output language format making it suitable to plug into any of the industrial design flows. A number of design experiments prove the usability of the discussed design flow.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 109.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 139.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 139.99
Price excludes VAT (USA)
  • Durable hardcover 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

Institutional subscriptions

Notes

  1. 1.

    The Formal Intermediate Format is patented with patent number: 1006354, 15/4/2009, from the Greek Industrial Property Organization.

  2. 2.

    This hardware compiler method is patented with patent number: 1005308, 5/10/2006, from the Greek Industrial Property Organization.

References

  1. B. Pangrle, D. Gajski, Design tools for intelligent silicon compilation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 6(6), 1098–1112 (1987)

    Article  Google Scholar 

  2. E. Girczyc, R. Buhr, J. Knight, Applicability of a subset of Ada as an algorithmic hardware description language for graph-based hardware compilation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 4(2), 134–142 (1985)

    Article  Google Scholar 

  3. P. Paulin, J. Knight, Algorithms for high-level synthesis. IEEE Des. Test Comput. 6(6), 18–31 (1989)

    Article  Google Scholar 

  4. I. Park, C. Kyung, Fast and near optimal scheduling in automatic data path synthesis, in Proceedings of the Design Automation Conference (DAC), pp. 680–685, San Francisco, CA, 1991

    Google Scholar 

  5. N. Park, A. Parker, Sehwa: a software package for synthesis of pipelined data path from behavioral specification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 7(3), 356–370 (1988)

    Article  Google Scholar 

  6. E. Girczyc, Loop winding—a data flow approach to functional pipelining, in Proceedings of the International Symposium on Circuits and Systems, pp. 382–385, Philadelphia, PA, May 1987

    Google Scholar 

  7. C. Tseng, D. Siewiorek, Automatic synthesis of data path on digital systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 5(3), 379–395 (1986)

    Article  Google Scholar 

  8. F. Kurdahi, A. Parker, REAL: a program for register allocation, in Proceedings of the Design Automation Conference (DAC), pp. 210–215, Miami Beach, FL, June 1987

    Google Scholar 

  9. C. Huang, Y. Chen, Y. Lin, Y. Hsu, Data path allocation based on bipartite weighted matching, in Proceedings of the Design Automation Conference (DAC), pp. 499–504, Orlando, FL, June 1990

    Google Scholar 

  10. F. Tsay, Y. Hsu, Data path construction and refinement, in Digest of Technical Papers, International Conference on Computer-Aided Design (ICCAD), pp. 308–311, Santa Clara, CA, November 1990

    Google Scholar 

  11. R. Camposano, W. Rosenstiel, Synthesizing circuits from behavioral descriptions. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 8(2), 171–180 (1989)

    Article  Google Scholar 

  12. S. Johnson, Synthesis of Digital Designs from Recursion Equations (MIT Press, Cambridge, MA, 1984)

    Google Scholar 

  13. M. Barbacci, G. Barnes, R. Cattell, D. Siewiorek, The ISPS computer description language. Report CMU-CS-79-137, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, 1979

    Google Scholar 

  14. P. Marwedel, The MIMOLA design system: tools for the design of digital processors, in Proceedings of the 21st Design Automation Conference (DAC), pp. 587–593, IEEE Press, Piscataway, NJ, 1984

    Google Scholar 

  15. A. Casavant, M. D’Abreu, M. Dragomirecky, D. Duff, J. Jasica, M. Hartman, K. Hwang, W. Smith, A synthesis environment for designing DSP systems. IEEE Des. Test Comput. 6(2), 35–44 (1989)

    Article  Google Scholar 

  16. P. Paulin, J. Knight, Force-directed scheduling for the behavioral synthesis of ASICs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 8(6), 661–679 (1989)

    Article  Google Scholar 

  17. D. Gajski, L. Ramachandran, Introduction to high-level synthesis. IEEE Des. Test Comput. 11(4), 44–54 (1994)

    Article  Google Scholar 

  18. R. Walker, S. Chaudhuri, Introduction to the scheduling problem. IEEE Des. Test Comput. 12(2), 60–69 (1995)

    Article  Google Scholar 

  19. V. Berstis, The V compiler: automatic hardware design. IEEE Des. Test Comput. 6(2), 8–17 (1989)

    Article  Google Scholar 

  20. J. Fisher, Trace Scheduling: a technique for global microcode compaction. IEEE Trans. Comput. C-30(7), 478–490 (1981)

    Article  Google Scholar 

  21. A. Kuehlmann, R. Bergamaschi, Timing analysis in high-level synthesis, in Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design (ICCAD ‘92), pp. 349–354, Los Alamitos, CA, 1992

    Google Scholar 

  22. C. Papachristou, H. Konuk, A linear program driven scheduling and allocation method followed by an interconnect optimization algorithm, in Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC), Orlando, Florida, USA, pp. 77–83, June 1990

    Google Scholar 

  23. J. Biesenack, M. Koster, A. Langmaier, S. Ledeux, S. Marz, M. Payer, M. Pilsl, S. Rumler, H. Soukup, N. Wehn, P. Duzy, The Siemens high-level synthesis system CALLAS. IEEE Trans. Very Large Scale Integr. Syst. 1(3), 244–253 (1993)

    Article  Google Scholar 

  24. T. Filkorn, A method for symbolic verification of synchronous circuits, in Proceedings of the Comp Hardware Descr Lang and Their Application (CHDL 91), pp. 229–239, Marseille, 1991

    Google Scholar 

  25. A. Kalavade, E. Lee, A hardware-software codesign methodology for DSP applications. IEEE Des. Test Comput. 10(3), 16–28 (1993)

    Article  Google Scholar 

  26. R. Ernst, J. Henkel, T. Benner, Hardware-software cosynthesis for microcontrollers. IEEE Des. Test Comput. 10(4), 64–75 (1993)

    Article  Google Scholar 

  27. G. De Micheli, D. Ku, F. Mailhot, T. Truong, The Olympus synthesis system. IEEE Des. Test Comput. 7(5), 37–53 (1990)

    Article  Google Scholar 

  28. D. Thomas, J. Adams, H. Schmit, A model and methodology for hardware-software codesign. IEEE Des. Test Comput. 10(3), 6–15 (1993)

    Article  Google Scholar 

  29. C. Hoare, Communicating Sequential Processes (Prentice-Hall, Englewood Cliffs, NJ, 1985)

    MATH  Google Scholar 

  30. R. Gupta, G. De Micheli, Hardware-software cosynthesis for digital systems. IEEE Des. Test Comput. 10(3), 29–41 (1993)

    Article  Google Scholar 

  31. I. Bolsens, H. De Man, B. Lin, K. Van Rompaey, S. Vercauteren, D. Verkest, Hardware/software co-design of digital telecommunication systems. Proc. IEEE 85(3), 391–418 (1997)

    Article  Google Scholar 

  32. D. Genin, P. Hilfinger, J. Rabaey, C. Scheers, H. De Man, DSP specification using the SILAGE language, in Proceedings of the International Conference on Acoustics Speech Signal Process, pp. 1056–1060, Albuquerque, NM, 3–6 April 1990

    Google Scholar 

  33. P. Willekens et~al., Algorithm specification in DSP station using data flow language. DSP Appl. 3(1), 8–16 (1994)

    Google Scholar 

  34. N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud, The synchronous dataflow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991)

    Article  Google Scholar 

  35. M. Van Canneyt, Specification, simulation and implementation of a GSM speech codec with DSP station. DSP Multimed. Technol. 3(5), 6–15 (1994)

    Google Scholar 

  36. J. Buck, S. Ha, E. Lee, D. Messerschmitt, PTOLEMY: a framework for simulating and prototyping heterogeneous systems. Int. J. Comput. Simul. 4, 1–34 (1992)

    Google Scholar 

  37. R. Lauwereins, M. Engels, M. Ade, J. Peperstraete, GRAPE-II: a system level prototyping environment for DSP applications. IEEE Comput. 28(2), 35–43 (1995)

    Article  Google Scholar 

  38. M. Rafie et~al., Rapid design and prototyping of a direct sequence spread-spectrum ASIC over a wireless link. DSP Multimed. Technol. 3(6), 6–12 (1994)

    Google Scholar 

  39. L. Semeria, K. Sato, G. De Micheli, Synthesis of hardware models in C with pointers and complex data structures. IEEE Trans. VLSI Syst. 9(6), 743–756 (2001)

    Article  Google Scholar 

  40. R. Wilson, R. French, C. Wilson, S. Amarasinghe, J. Anderson, S. Tjiang, S.-W. Liao, C.-W. Tseng, M. Hall, M. Lam, J. Hennessy, Suif: an infrastructure for research on parallelizing and optimizing compilers. ACM SIPLAN Notices 28(9), 67–70 (1994)

    Google Scholar 

  41. A. Kountouris, C. Wolinski, Efficient scheduling of conditional behaviors for high-level synthesis. ACM Trans. Des. Autom. Electron. Syst. 7(3), 380–412 (2002)

    Article  Google Scholar 

  42. S. Gupta, R. Gupta, N. Dutt, A. Nikolau, Coordinated parallelizing compiler optimizations and high-level synthesis. ACM Trans. Des. Autom. Electron. Syst. 9(4), 441–470 (2004)

    Article  Google Scholar 

  43. W. Wang, A. Raghunathan, N. Jha, S. Dey, High-level synthesis of multi-process behavioral descriptions, in Proceedings of the 16th IEEE International Conference on VLSI Design (VLSI’03), ISBN: 0-7695-1868-0, pp. 467–473, 4–8 January 2003

    Google Scholar 

  44. Z. Gu, J. Wang, R. Dick, H. Zhou, Incremental exploration of the combined physical and behavioral design space, in Proceedings of the 42nd Annual Conference on Design. Automation DAC ‘05, pp. 208–213, Anaheim, CA, 13–17 June 2005

    Google Scholar 

  45. L. Zhong, N. Jha, Interconnect-aware high-level synthesis for low power, in Proceedings of the IEEE/ACM International Conference Computer-Aided Design, ISBN: 0-7803-7607-2, pp. 110–117, November 2002

    Google Scholar 

  46. C. Huang, S. Ravi, A. Raghunathan, N. Jha, Generation of heterogeneous distributed architectures for memory-intensive applications through high-level synthesis. IEEE Trans. Very Large Scale Integr. 15(11), 1191–1204 (2007)

    Article  Google Scholar 

  47. K. Wakabayashi, C-based synthesis experiences with a behavior synthesizer, “Cyber”, in Proceedings of the Design Automation and Test in Europe Conference, ISBN: 0-7695-0078-1, pp. 390–393, Munich, 9–12 March 1999

    Google Scholar 

  48. W. Wang, T. Tan, J. Luo, Y. Fei, L. Shang, K. Vallerio, L. Zhong, A. Raghunathan, N. Jha, A comprehensive high-level synthesis system for control-flow intensive behaviors, in Proceedings of the 13th ACM Great Lakes Symposium on VLSI GLSVLSI ‘03, ISBN:1-58113-677-3, pp. 11–14, Washington, DC, 28–29 April 2003

    Google Scholar 

  49. B. Gal, E. Casseau, S. Huet, Dynamic memory access management for high-performance DSP applications using high-level synthesis. IEEE Trans. Very Large Scale Integr. 16(11), 1454–1464 (2008)

    Article  Google Scholar 

  50. S. Gupta, R. Gupta, N. Dutt, A. Nicolau, Dynamically increasing the scope of code motions during the high-level synthesis of digital circuits, in Proceedings of the IEEE Conference Computers and Digital Techniques, ISSN: 1350–2387, vol. 150, no. 5, pp. 330–337, 22 September 2003

    Google Scholar 

  51. K. Wakabayashi, H. Tanaka, Global scheduling independent of control dependencies based on condition vectors, in Proceedings of the 29th ACM/IEEE Design Automation Conference (DAC), ISBN: 0-8186-2822-7, pp. 112–115, Anaheim, CA, 8–12 June 1992

    Google Scholar 

  52. E. Martin, O. Santieys, J. Philippe, GAUT, an architecture synthesis tool for dedicated signal processors, in Proceedings of the IEEE International European Design Automation Conference (Euro-DAC), pp. 14–19, Hamburg, September 1993

    Google Scholar 

  53. M. Molina, R. Ruiz-Sautua, P. Garcia-Repetto, R. Hermida, Frequent-pattern-guided multilevel decomposition of behavioral specifications. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 28(1), 60–73 (2009)

    Article  Google Scholar 

  54. K. Avnit, V. D’Silva, A. Sowmya, S. Ramesh, S. Parameswaran, Provably correct on-chip communication: a formal approach to automatic protocol converter synthesis. ACM Trans. Des. Autom. Electron. Syst. 14(2), 19 (2009)

    Article  Google Scholar 

  55. J. Keinert, M. Streubuhr, T. Schlichter, J. Falk, J. Gladigau, C. Haubelt, J. Teich, M. Meredith, SystemCoDesigner—an automatic ESL synthesis approach by design space exploration and behavioral synthesis for streaming applications. ACM Trans. Des. Autom. Electron. Syst. 14(1), 1 (2009)

    Article  Google Scholar 

  56. S. Kundu, S. Lerner, R. Gupta, Translation validation of high-level synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(4), 566–579 (2010)

    Article  Google Scholar 

  57. S. Paik, I. Shin, T. Kim, Y. Shin, HLS-l: a high-level synthesis framework for latch-based architectures. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(5), 657–670 (2010)

    Article  Google Scholar 

  58. A. Raghunathan, S. Dey, N. Jha, Register-transfer level estimation techniques for switching activity and power consumption, in Digest of Technical Papers, International Conference on Computer-Aided Design (ICCAD), ISBN: 0-8186-7597-7, pp. 158–165, San Jose, CA, 10–14 November 1996

    Google Scholar 

  59. J. Rabaey, L. Guerra, R. Mehra, Design guidance in the power dimension, in Proceedings of the 1995 International Conference on Acoustics, Speech, and Signal Processing, ISBN: 0-7803-2431-5, pp. 2837–2840, Detroit, MI, 9–12 May 1995

    Google Scholar 

  60. R. Mehra, J. Rabaey, Exploiting regularity for low-power design, in Digest of Technical Papers, International Conference on Computer-Aided Design (ICCAD), ISBN: 0-8186-7597-7, pp. 166–172, San Jose, CA, November 1996

    Google Scholar 

  61. A. Raghunathan, N. Jha, Behavioral synthesis for low power, in Proceedings of the International Conference on Computer Design (ICCD), ISBN: 0-8186-6565-3, pp. 318–322, Cambridge, MA, 10–12 October 1994

    Google Scholar 

  62. L. Goodby, A. Orailoglu, P. Chau, Microarchitecture synthesis of performance-constrained low-power VLSI designs, in Proceedings of the International Conference on Computer Design (ICCD), ISBN: 0-8186-6565-3, pp. 323–326, Cambridge, MA, 10–12 October 1994

    Google Scholar 

  63. E. Musoll, J. Cortadella, Scheduling and resource binding for low power, in Proceedings of the Eighth Symposium on System Synthesis, ISBN: 0-8186-7076-2, pp. 104–109, Cannes, 13–15 September 1995

    Google Scholar 

  64. N. Kumar, S. Katkoori, L. Rader, R. Vemuri, Profile-driven behavioral synthesis for low-power VLSI systems. IEEE Des. Test Comput. 12(3), 70–84 (1995)

    Article  Google Scholar 

  65. R. Martin, J. Knight, Power-profiler: optimizing ASICs power consumption at the behavioral level, in Proceedings of the Design Automation Conference (DAC), ISBN: 0-89791-725-1, pp. 42–47, San Francisco, CA, 1995

    Google Scholar 

  66. I. Issenin, E. Brockmeyer, B. Durinck, N.D. Dutt, Data-reuse-driven energy-aware cosynthesis of scratch pad memory and hierarchical bus-based communication architecture for multiprocessor streaming applications. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(8), 1439–1452 (2008)

    Article  Google Scholar 

  67. M. Dossis, Intermediate Predicate Format for design automation tools. J. Next Gener. Inform. Technol. 1(1), 100–117 (2010)

    Article  Google Scholar 

  68. U. Nilsson, J. Maluszynski, Logic Programming and Prolog, 2nd edn. (John Wiley & Sons Ltd., Chichester, 1995)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TEI of Western Macedonia, Kastoria Campus, Fourka Area, Kastoria, 52100, Greece

    Michael Dossis

Authors
  1. Michael Dossis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Dossis .

Editor information

Editors and Affiliations

  1. Technological Educational Institute of Western Greece, Embedded System Design and Application Laboratory (ESDA), Antirio, Greece

    Georgios Keramidas

  2. Technological Educational Institute of Western Greece, Embedded System Design and Application Laboratory (ESDA), Antirio, Greece

    Nikolaos Voros

  3. Chair for Embedded Systems for Information Technology (ESIT), Ruhr Universität Bochum, Bochum, Germany

    Michael Hübner

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Dossis, M. (2017). Formal Design Flows for Embedded IoT Hardware. In: Keramidas, G., Voros, N., Hübner, M. (eds) Components and Services for IoT Platforms. Springer, Cham. https://doi.org/10.1007/978-3-319-42304-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-42304-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-42302-9

  • Online ISBN: 978-3-319-42304-3

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation