Skip to main content
SpringerLink
Log in

Related Work and Outlook

  • Chapter
  • First Online:
Correct-by-Construction Approaches for SoC Design

Abstract

Chapter 7 summarizes related work. We discuss the system-level verification literature and SoC design literature. Key concepts covered in this chapter include literature related to requirements, modelling and analysis techniques for component-based design of systems.

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

References

  1. K. Avnit, V. D’Silva, A. Sowmya, S. Ramesh, S. Parameswaran, A formal approach to the protocol converter problem. Design, Automation and Test in Europe, 2008. Date ’08, pp. 294–299, Mar 2008

    Google Scholar 

  2. 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. Design Autom. Electr. Syst. 14(2) (2009)

    Google Scholar 

  3. S. Baruah, H. Li, L. Stougie, Towards the design of certifiable mixed-criticality systems. In 16th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2010 (IEEE, Stockholm, 2010), pp. 13–22

    Google Scholar 

  4. A. Basu, R.S. Mitra, P. Marwedel, Interface synthesis for embedded applications in a co-design environment. In 11th IEEE International Conference on VLSI Design, pp. 85–90, 1998

    Google Scholar 

  5. L. Benini, Application specific NoC design. In DATE ’06: Proceedings of the Conference on Design, Automation and Test in Europe (European Design and Automation Association, Belgium, 2006), pp. 491–495

    Google Scholar 

  6. L. Benini, G. de Micheli, System-level power optimization: techniques and tools. ACM Trans. Design Autom. Electr. Syst. 5(2), 115–192 (2000)

    Article  Google Scholar 

  7. L. Benini, G. De Micheli, Networks on chips: a new SoC paradigm. Computer 35(1), 70–78 (2002)

    Article  Google Scholar 

  8. A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, R. de Simone, The synchronous languages 12 years later. Proc. IEEE 91(1), 64–83 (2003)

    Article  Google Scholar 

  9. G. Berry, A hardware implementation of pure Esterel. In International Workshop on Formal Methods in VLSI Design, Jan 1991

    Google Scholar 

  10. G. Berry, G. Gonthier, The ESTEREL synchronous programming language. Sci. Comput. Program. 19, 87–152 (1992)

    Article  MATH  Google Scholar 

  11. G. Berry, E. Sentovich, Multiclock esterel. In CHARME ’01: Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (Springer, London, 2001), pp. 110–125

    Google Scholar 

  12. G. Berry, L. Blanc, A. Bouali, J. Dormoy, Top-level validation of system-on-chip in Esterel studio. 7th IEEE International High-Level Design Validation and Test Workshop, pp. 36–41, Oct 2002

    Google Scholar 

  13. T. Bjerregaard, S. Mahadevan, A survey of research and practices of network-on-chip. ACM Comput. Surv. 38(1), 1 (2006)

    Article  Google Scholar 

  14. G. Borriello, A new interface specification methodology and its application to transducer synthesis. Ph.D. thesis, University of California, Berkeley, 1988

    Google Scholar 

  15. J. Cao, A. Nymeyer, Formally synthesising a protocol converter: a case study. In Proceedings of the 14th International Conference on Implementation and Application of Automata, CIAA ’09 (Springer, Berlin, 2009), pp. 249–252

    Google Scholar 

  16. L.P. Carloni, F. De Bernardinis, A.L. Sangiovanni-Vincentelli, M. Sgroi, The art and science of integrated systems design. In Proceedings of the 28th European Solid-State Circuits Conference (ESSCIRC 2002), pp. 25–36, Sep 2002

    Google Scholar 

  17. W.O. Cesario, D. Lyonnard, G. Nicolescu, Y. Paviot, S. Yoo, A.A. Jerraya, L. Gauthier, M. Diaz-Nava, Multiprocessor SoC platforms: a component-based design approach. Design Test Comput. IEEE 19(6), 52–63 (2002)

    Article  Google Scholar 

  18. A. Chakraborty, M.R. Greenstreet, Efficient self-timed interfaces for crossing clock domains. In ASYNC ’03: Proceedings of the 9th International Symposium on Asynchronous Circuits and Systems (IEEE Computer Society, Washington, 2003), p. 78

    Google Scholar 

  19. A. Chattopadhyay, Z. Zilic, GALDS: a complete framework for designing multiclock ASICs and SoCs. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 13(6), 641–654 (2005)

    Google Scholar 

  20. Y.-Y. Chen, T.-Y. Juang, Vulnerability Analysis and Risk Assessment for SoCs Used in Safety-Critical Embedded Systems (InTech, 2009)

    Google Scholar 

  21. P. Chou, R.B. Ortega, G. Borriello, Interface co-synthesis techniques for embedded systems. In ICCAD, pp. 280–287, 1995

    Google Scholar 

  22. E.M. Clarke, O. Grumberg, D. Peled, Model Checking (MIT Press, Massachusetts, 2000)

    Google Scholar 

  23. L. de Alfaro, T.A. Henzinger, Interface automata. In ESEC / SIGSOFT FSE, pp. 109–120, 2001

    Google Scholar 

  24. L. de Alfaro, T.A. Henzinger, Interface theories for component-based design. In EMSOFT, ed. by T.A. Henzinger, C.M. Kirsch. Lecture Notes in Computer Science, vol 2211 (Springer, New York, 2001), pp. 148–165

    Google Scholar 

  25. V. D’Silva, S. Ramesh, A. Sowmya, Bridge over troubled wrappers: automated interface synthesis. In VLSI Design (IEEE Computer Society, Washington, 2004), pp. 189–194

    Google Scholar 

  26. V. D’Silva, S. Ramesh, A. Sowmya, Synchronous protocol automata: a framework for modelling and verification of SoC communication architectures. In DATE (IEEE Computer Society, Washington, 2004), pp. 390–395

    Google Scholar 

  27. V. D’Silva, S. Ramesh, A. Sowmya, Synchronous protocol automata: a framework for modelling and verification of SoC communication architectures. IEE Proc. Comput. Digital Tech. 152(1), 20–27 (2005)

    Article  Google Scholar 

  28. M. Fujita, Synthesizing, verifying, and debugging SoC with FSM-based specification of on-chip communication protocols. In ATVA 2011, ed. by T. Bultan, P.-A. Hsiung. Lecture Notes in Computer Science, vol 6996 (Springer, Berlin, 2011)

    Google Scholar 

  29. D.D. Gajski, A.C.-H. Wu, V. Chaiyakul, S. Mori, T. Nukiyama, P. Bricaud, Essential issues for IP reuse. In ASP-DAC 2000: Proceedings of the Asia and South Pacific Design Automation Conference, pp. 37–42, 2000

    Google Scholar 

  30. A. Ghosh, S. Tjiang, R. Chandra, System modeling with systemc. In Proceedings of the 4th International Conference on ASIC, pp. 18–20, 2001

    Google Scholar 

  31. C. Gierds, A.J. Mooij, K. Wolf, Reducing adapter synthesis to controller synthesis. IEEE Trans. Services Comput. 5(1), 72–85 (2012)

    Article  Google Scholar 

  32. M.R. Greenstreet, STARI: a technique for high-bandwidth communication. Ph.D. thesis, Princeton University, 1993

    Google Scholar 

  33. P. Guerrier, A. Greiner, A generic architecture for on-chip packet-switched interconnections. In DATE ’00: Proceedings of the Conference on Design, Automation and Test in Europe (ACM, New York, 2000), pp. 250–256

    Google Scholar 

  34. N. Halbwachs, Synchronous Programming of Reactive Systems. Kluwer International Series in Engineering and Computer Science (Kluwer, Princeton, 1994)

    Google Scholar 

  35. J. Henkel, Closing the SoC design gap. Computer 36(9), 119–121 (2003)

    Article  Google Scholar 

  36. C.A.R. Hoare, Communicating Sequential Processes (Prentice Hall International, Saddle River, 1985)

    MATH  Google Scholar 

  37. T.B. Ismail, J.M. Daveau, K. O’Brien, A.A. Jerraya, A system level communication approach for hardware/software systems. Microprocess. Microsyst. 20(3), 149–157 (1996)

    Article  Google Scholar 

  38. S. Jiang, R. Kumar, Supervisory control of discrete event systems with CTL ∗  temporal logic specifications. SIAM J. Control Optim. 44(6), 2079–2103 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  39. G. Kahn, The semantics of a simple language for parallel programming. Information Processing (Elsevier, North Holland, 1974)

    Google Scholar 

  40. M. Keating, P. Bircaud, Reuse Methodology Manual for System-On-A-Chip Designs (Springer, New York, 2002)

    Google Scholar 

  41. K. Keutzer, S. Malik, R. Newton, J. Rabaey, A. Sangiovanni-vincentelli, System-level design: orthogonalization of concerns and platform-based design. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 19, 1523–1543 (2000)

    Article  Google Scholar 

  42. R. Kumar, S.S. Nelvagal, Convertibility verification using supervisory control techniques. In IEEE International Symposium on Computer-Aided Control System Design (IEEE Computer Society, Washington, 1996), pp. 32–37

    Google Scholar 

  43. R. Kumar, S. Nelvagal, S.I. Marcus, A discrete event systems approach for protocol conversion. Discrete Event Dyn. Syst. 7(3), 295–315 (1997)

    Article  MATH  Google Scholar 

  44. O. Kupferman, M.Y. Vardi, P. Wolper, Module checking. Inform. Comput. 164(2), 322–344 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  45. J. Lefebvre, Esterel v7 Reference Manual-Initial Standardization Proposal, 2005

    Google Scholar 

  46. J. Li, F. Xie, T. Ball, V. Levin, C. McGarvey, Formalizing hardware/software interface specifications. In ASE, ed. by P. Alexander, C.S. Pasareanu, J.G. Hosking (IEEE, New York, 2011), pp. 143–152

    Google Scholar 

  47. M. Lindwer, M.R. Pedersen, High-performance imaging subsystems and their integration in mobile devices. In Proceedings of the Conference on Design, Automation and Test in Europe, DATE ’13 (EDA Consortium, San Jose, 2013), pp. 170–170

    Google Scholar 

  48. C.D. Locke, D.R. Vogel, L. Lucas, J.B. Goodenough, Generic avionics software. specification. Technical Report, DTIC Document, 1990

    Google Scholar 

  49. N.A. Lynch, M.R. Tuttle, Hierarchical correctness proofs for distributed algorithms. In PODC, ed. by F.B. Schneider (ACM, New York, 1987), pp. 137–151

    Google Scholar 

  50. P. Magarshack, P.G. Paulin, System-on-chip beyond the nanometer wall. Proceedings of the Design Automation Conference, pp. 419–424, June 2003

    Google Scholar 

  51. F. Maraninchi, Y. Rémond, Argos: an automaton-based synchronous language. Comput. Lang. 27(1–3), 61–92 (2001)

    Article  MATH  Google Scholar 

  52. J. Mekie, S. Chakraborty, D.K. Sharma, G. Venkataramani, P.S. Thiagarajan, Interface design for rationally clocked gals systems. In 12th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC’06) (IEEE Computer Society, Washington, 2006), pp. 160–171

    Google Scholar 

  53. R. Milner, Communication and Concurrency (Prentice Hall International, Upper Saddle River, 1989)

    MATH  Google Scholar 

  54. S. Narayan, D. Gajski, Interfacing incompatible protocols using interface process generation. In 32nd Design Automation Conference, pp. 468–473, 1995

    Google Scholar 

  55. D.L. Parnas, Use of abstract interfaces in the development of software for embedded computing systems. Technical Report 8047 (Naval research lab, Washington, 1977)

    Google Scholar 

  56. D.L. Parnas, Really rethinking ‘formal methods’. Computer 43(1), 28–34 (2010)

    Article  Google Scholar 

  57. R. Passerone, L. de Alfaro, T.A. Henzinger, A.L. Sangiovanni-Vincentelli, Convertibility verification and converter synthesis: two faces of the same coin. In International Conference on Computer Aided Design ICCAD, 2002

    Google Scholar 

  58. R. Pellizzoni, P. Meredith, M.-Y. Nam, M. Sun, M. Caccamo, L. Sha, Handling mixed-criticality in soc-based real-time embedded systems. In Proceedings of the Seventh ACM International Conference on Embedded Software, EMSOFT ’09 (ACM, New York, 2009), pp. 235–244

    Google Scholar 

  59. I. Radojevic, Z. Salcic, P.S. Roop, Mccharts and multiclock fsms for modelling large scale systems. In Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’2007) (IEEE Computer Society, Washington, 2007), pp. 3–12

    Google Scholar 

  60. V. Raghunathan, M.B. Srivastava, R.K. Gupta, A survey of techniques for energy efficient on-chip communication. In DAC ’03: Proceedings of the 40th Conference on Design Automation (ACM, New York, 2003), pp. 900–905

    Google Scholar 

  61. P.J.G. Ramadge, W.M. Wonham, The control of discrete event systems. Proc. IEEE 77, 81–98 (1989)

    Article  Google Scholar 

  62. D.I. Rich, The evolution of system verilog. IEEE Design Test Comput. 20(4), 82–84 (2003)

    Article  Google Scholar 

  63. P.S. Roop, A. Sowmya, S. Ramesh, Forced simulation: a technique for automating component reuse in embedded systems. ACM Trans. Design Autom. Electr. Syst. 6(4), 602–628 (2001)

    Article  Google Scholar 

  64. P.S. Roop, A. Girault, R. Sinha, G. Goessler, Specification enforcing refinement for convertibility verification. In International Conference on Application of Concurrency to System Design, ACSD’09 (IEEE Computer Society, Augsburg, 2009), pp. 148–157

    Google Scholar 

  65. I. Sander, A. Jantsch, System modeling and transformational design refinement in forsyde [formal system design]. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 23(1), 17–32 (2004)

    Article  Google Scholar 

  66. A.L. Sangiovanni-Vincentelli, M. Sgroi, L. Lavagno, Formal models for communication-based design. In CONCUR ’00: Proceedings of the 11th International Conference on Concurrency Theory (Springer, London, 2000), pp. 29–47

    Google Scholar 

  67. A. Sangiovanni-Vincentelli, L. Carloni, F. De Bernardinis, M. Sgroi, Benefits and challenges for platform-based design. In DAC ’04: Proceedings of the 41st Annual Conference on Design Automation (ACM, New York, 2004), pp. 409–414

    Google Scholar 

  68. SCADE, Scade suite, http://www.esterel-technologies.com/products/scade-suite/. Accessed 30 Apr 2013

  69. C.L. Seitz, System timing. Introduction to VLSI Systems, Chapter 7 (Addison-Wesley, Reading, 1980)

  70. M. Sgroi, M. Sheets, A. Mihal, K. Keutzer, S. Malik, J. Rabaey, A. Sangiovanni-Vencentelli, Addressing the system-on-a-chip interconnect woes through communication-based design. In DAC ’01: Proceedings of the 38th Conference on Design Automation (ACM, New York, 2001), pp. 667–672

    Google Scholar 

  71. C.-H. Shih, Y.-C. Yang, C.-C. Yen, J.-D. Huang, J.-Y. Jou, Fsm-based formal compliance verification of interface protocols. Inform. Sci. Eng. 26, 1601–1617 (2010)

    Google Scholar 

  72. R. Sinha, P.S. Roop, S. Basu, Z. Salcic, A module checking based converter synthesis approach for SoCs. In IEEE International Conference on VLSI Design (IEEE Computer Society, Washington, 2008), pp. 492–501

    Google Scholar 

  73. R. Sinha, P.S. Roop, S. Basu, Soc design approach using convertibility verification. EURASIP J. Embed. Syst. 2008 (2008)

    Google Scholar 

  74. R. Sinha, P.S. Roop, S. Basu, Z. Salcic, Multi-clock SoC design using protocol conversion. In Design and Test Europe (DATE) (IEEE, New York, 2009), pp. 123–128

    Google Scholar 

  75. R. Sinha, P.S. Roop, Z. Salcic, S. Basu, Correct-by-construction multi-component soc design. In DATE, ed. by W. Rosenstiel, L. Thiele (IEEE, New York, 2012), pp. 647–652

    Google Scholar 

  76. R. Sinha, A. Girault, G. Goessler, P.S. Roop, Formal system-on-chip design using incremental converter synthesis. Technical Report TBA, INRIA, Rhone-Alps, 2013

    Google Scholar 

  77. F. Somenzi, R. Bloem, Efficient büchi automata from ltl formulae. In Computer Aided Verification (Springer, New York, 2000), pp. 248–263

    Google Scholar 

  78. I. Sommerville, P. Sawyer, Requirements Engineering: A Good Practice Guide, 1st edn. (Wiley, New York, 1997)

    MATH  Google Scholar 

  79. S.M. Suhaib, Formal methods for intellectual property composition across synchronization domains. Ph.D. thesis, Virginia Polytechnic Institute and State University, 2007

    Google Scholar 

  80. A. van Lamsweerde, Goal-oriented requirements engineering: a guided tour. In Proceedings of 5th IEEE International Symposium on Requirements Engineering, 2001, pp. 249–262, 2001

    Google Scholar 

  81. K.E. Wiegers, Automating requirements management. Software Development 7(7), 1–5 (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Electrical and Computer Engineering, The University of Auckland, Auckland, New Zealand

    Roopak Sinha & Parthasarathi Roop

  2. Department of Computer Science, Iowa State University, Ames, IA, USA

    Samik Basu

Authors
  1. Roopak Sinha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Parthasarathi Roop
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Samik Basu
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer Science+Business Media New York

About this chapter

Cite this chapter

Sinha, R., Roop, P., Basu, S. (2014). Related Work and Outlook. In: Correct-by-Construction Approaches for SoC Design. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-7864-5_7

Download citation

  • DOI: https://doi.org/10.1007/978-1-4614-7864-5_7

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4614-7863-8

  • Online ISBN: 978-1-4614-7864-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation