Skip to main content

Einleitung

  • Chapter
  • First Online:
Book cover Digitale Hardware/Software-Systeme

Part of the book series: eXamen.press ((EXAMEN,volume 0))

  • 5081 Accesses

Zusammenfassung

Dieses einleitende Kapitel vermittelt einen Einblick, warum die Verifikation ein unverzichtbarer Bestandteil des Entwurfs von digitalen Hardware/Software-Systemen darstellt. Dabei werden die wesentlichen Aspekte der Verifikation vorgestellt.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 39.99
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

  1. Lee, E. A. und A. L. Sangiovanni-Vincentelli: A Framework for Comparing Models of Computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12):1217–1229, 1998.

    Article  Google Scholar 

  2. Evans, A., A. Silburt, G. Vrckovnik, T. Brown, M. Dufresne, G. Hall, T. Ho und Y. Liu: Functional Verification of Large ASICs. In: Proceedings of the Design Automation Conference (DAC), Seiten 650–655, 1998.

    Google Scholar 

  3. Floyd, R. W.: Assigning Meaning to Programs. In: Proceedings of the Symposium of Applied Mathematics, Seiten 19–32, 1967.

    Google Scholar 

  4. Zhu, C., Z. P. Gu, R. P. Dick und L. Shang: Reliable Multiprocessor System-On-Chip Synthesis. In: Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), Seiten 239–244, 2007.

    Google Scholar 

  5. Wolf, Wayne, Ahmed Amine Jerraya und Grant Martin: Multiprocessor System-on-Chip (MPSoC) Technology. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(10):1701–1713, 2008.

    Article  Google Scholar 

  6. OSCI TLM Working Group: OSCI TLM-2.0 Language Reference Manual, 2009. Version JA32, http://www.systemc.org.

  7. Kienhuis, B., E. Deprettere, K. Vissers und P. van der Wolf: An Approach for Quantitative Analysis of Application-Specific Dataflow Architectures. In: Proceedings of the Conference on Application-Specific Systems, Architectures and Processors (ASAP), Seiten 338–349, 1997.

    Google Scholar 

  8. ller, K.-H.: Ausgangsdaten für Qualitätsmetriken – Eine Fundgrube für Analysen. In: Ebert, C. und R. Dumke(Herausgeber): Software-Metriken in der Praxis, Seiten 105 – 116. Springer, Berlin, 1996.

    Google Scholar 

  9. Gerstlauer, A., C. Haubelt, A. D. Pimentel, T. P. Stefanov, D. D. Gajski und J. Teich: Electronic System-Level Synthesis Methodologies. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28(10):1517–1530, 2009.

    Article  Google Scholar 

  10. Kripke, S. A.: A Completeness Theorem in Modal Logic. The Journal of Symbolic Logic, 24(1):1–14, 1959.

    Article  MATH  MathSciNet  Google Scholar 

  11. Moore, G.: Cramming More Components onto Integrated Circuits. Electronics, 38:114–117, 1965.

    Google Scholar 

  12. Gajski, D. D., J. Zhu, R. Dömer, A. Gerstlauer und S. Zhao: SpecC: Specification Language and Design Methodology. Kluwer Academic Publishers, 2000.

    Google Scholar 

  13. Schneider, K.: Verification of Reactive Systems – Formal Methods and Algorithms. Springer, Berlin, Heidelberg, 2004.

    MATH  Google Scholar 

  14. Cook, S. A.: The Complexity of Theorem-Proving Procedures. In: Proceedings of the Symposium on Theory of Computing (STOC), Seiten 151–158, 1971.

    Google Scholar 

  15. Pasricha, S., N. Dutt, E. Bozorgzadeh und M. Ben-Romdhane: FABSYN: Floorplan-aware Bus Architecture Synthesis. IEEE Transactions on Very Large Scale Integrated Systems, 14(3):241–253, 2006.

    Article  Google Scholar 

  16. Gajski, D. D., F. Vahid, S. Narayan und J. Gong: Specification and Design of Embedded Systems. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1994.

    MATH  Google Scholar 

  17. Thiele, L. und E. Wandeler: Performance Analysis of Distributed Embedded Systems. In: Embedded Systems Handbook, Seiten 15.1–15.18. CRC Press, Boca Raton, FL, 2006.

    Google Scholar 

  18. Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the Symposium on Foundations of Computer Science, Seiten 46–57, 1977.

    Google Scholar 

  19. Hoare, C. A. R.: An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10):576–580, 1969.

    Article  MATH  Google Scholar 

  20. Bergeron, J.: Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, Dordrecht, 2003. 2. Auflage.

    MATH  Google Scholar 

  21. Sebastiani, Roberto: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, 3:141–224, 2007.

    MATH  MathSciNet  Google Scholar 

  22. Davis, M., G. Logemann und D. Loveland: A Machine Program for Theorem-Proving. Communications of the ACM, 5(7):394–397, 1962.

    Article  MATH  MathSciNet  Google Scholar 

  23. Teich, J. und C. Haubelt: Digitale Hardware/Software-Systeme – Synthese und Optimierung. Springer, Berlin, Heidelberg, 2007. 2. erweiterte Auflage.

    MATH  Google Scholar 

  24. Brand, D.: Verification of Large Synthesized Designs. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 534–537, 1993.

    Google Scholar 

  25. Turing, A.: On Computable Numbers With An Application To The Entscheidungs Problem. In: Proceedings of The London Mathematical Society, Band 42 der Reihe 2, Seiten 230–265, 1937.

    Google Scholar 

  26. Liggesmeyer, P.: Software-Qualität – Testen, Analysieren und Verifizieren von Software. Spektrum Akademischer Verlag, Heidelberg, Berlin, 2002.

    MATH  Google Scholar 

  27. Gajski, D. D. und R. H. Kuhn: New VLSI Tools. IEEE Computer, 16(12):11–14, 1983.

    Google Scholar 

  28. SystemC Verification Working Group: SystemC Verification Standard Specification, 2006. Version 1.0e, http://www.systemc.org.

  29. Kernighan, B. W. und D. Ritchie: The C Programming Language. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1988. 2. Auflage.

    Google Scholar 

  30. Gödel, Kurt: über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931.

    Google Scholar 

  31. IEEE: IEEE Standard Glossary of Software Engineering Terminology. IEEE Std 610.12-1990, 1990.

    Google Scholar 

  32. Strahm, T.: Logik in Informatik, Mathematik und Philosophie, 1999. Vortrag anlässlich der Veranstaltung Theodor-Kocher-Preis 1998 der Universität Bern.

    Google Scholar 

  33. Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.

    Article  MATH  Google Scholar 

  34. ITRS: International Technology Roadmap for Semiconductors – System Drivers. Technischer Bericht, ITRS, 2007. http://www.itrs.net/.

  35. Lee, E. A. und A. L. Sangiovanni-Vincentelli: A Framework for Comparing Models of Computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(12):1217–1229, 1998.

    Article  Google Scholar 

  36. Evans, A., A. Silburt, G. Vrckovnik, T. Brown, M. Dufresne, G. Hall, T. Ho und Y. Liu: Functional Verification of Large ASICs. In: Proceedings of the Design Automation Conference (DAC), Seiten 650–655, 1998.

    Google Scholar 

  37. Floyd, R. W.: Assigning Meaning to Programs. In: Proceedings of the Symposium of Applied Mathematics, Seiten 19–32, 1967.

    Google Scholar 

  38. Zhu, C., Z. P. Gu, R. P. Dick und L. Shang: Reliable Multiprocessor System-On-Chip Synthesis. In: Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), Seiten 239–244, 2007.

    Google Scholar 

  39. Wolf, Wayne, Ahmed Amine Jerraya und Grant Martin: Multiprocessor System-on-Chip (MPSoC) Technology. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(10):1701–1713, 2008.

    Article  Google Scholar 

  40. OSCI TLM Working Group: OSCI TLM-2.0 Language Reference Manual, 2009. Version JA32, http://www.systemc.org.

  41. Kienhuis, B., E. Deprettere, K. Vissers und P. van der Wolf: An Approach for Quantitative Analysis of Application-Specific Dataflow Architectures. In: Proceedings of the Conference on Application-Specific Systems, Architectures and Processors (ASAP), Seiten 338–349, 1997.

    Google Scholar 

  42. ller, K.-H.: Ausgangsdaten für Qualitätsmetriken – Eine Fundgrube für Analysen. In: Ebert, C. und R. Dumke(Herausgeber): Software-Metriken in der Praxis, Seiten 105 – 116. Springer, Berlin, 1996.

    Google Scholar 

  43. Gerstlauer, A., C. Haubelt, A. D. Pimentel, T. P. Stefanov, D. D. Gajski und J. Teich: Electronic System-Level Synthesis Methodologies. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28(10):1517–1530, 2009.

    Article  Google Scholar 

  44. Kripke, S. A.: A Completeness Theorem in Modal Logic. The Journal of Symbolic Logic, 24(1):1–14, 1959.

    Article  MATH  MathSciNet  Google Scholar 

  45. Moore, G.: Cramming More Components onto Integrated Circuits. Electronics, 38:114–117, 1965.

    Google Scholar 

  46. Gajski, D. D., J. Zhu, R. Dömer, A. Gerstlauer und S. Zhao: SpecC: Specification Language and Design Methodology. Kluwer Academic Publishers, 2000.

    Google Scholar 

  47. Schneider, K.: Verification of Reactive Systems – Formal Methods and Algorithms. Springer, Berlin, Heidelberg, 2004.

    MATH  Google Scholar 

  48. Cook, S. A.: The Complexity of Theorem-Proving Procedures. In: Proceedings of the Symposium on Theory of Computing (STOC), Seiten 151–158, 1971.

    Google Scholar 

  49. Pasricha, S., N. Dutt, E. Bozorgzadeh und M. Ben-Romdhane: FABSYN: Floorplan-aware Bus Architecture Synthesis. IEEE Transactions on Very Large Scale Integrated Systems, 14(3):241–253, 2006.

    Article  Google Scholar 

  50. Gajski, D. D., F. Vahid, S. Narayan und J. Gong: Specification and Design of Embedded Systems. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1994.

    MATH  Google Scholar 

  51. Thiele, L. und E. Wandeler: Performance Analysis of Distributed Embedded Systems. In: Embedded Systems Handbook, Seiten 15.1–15.18. CRC Press, Boca Raton, FL, 2006.

    Google Scholar 

  52. Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the Symposium on Foundations of Computer Science, Seiten 46–57, 1977.

    Google Scholar 

  53. Hoare, C. A. R.: An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10):576–580, 1969.

    Article  MATH  Google Scholar 

  54. Bergeron, J.: Writing Testbenches: Functional Verification of HDL Models. Kluwer Academic Publishers, Dordrecht, 2003. 2. Auflage.

    MATH  Google Scholar 

  55. Sebastiani, Roberto: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, 3:141–224, 2007.

    MATH  MathSciNet  Google Scholar 

  56. Davis, M., G. Logemann und D. Loveland: A Machine Program for Theorem-Proving. Communications of the ACM, 5(7):394–397, 1962.

    Article  MATH  MathSciNet  Google Scholar 

  57. Teich, J. und C. Haubelt: Digitale Hardware/Software-Systeme – Synthese und Optimierung. Springer, Berlin, Heidelberg, 2007. 2. erweiterte Auflage.

    MATH  Google Scholar 

  58. Brand, D.: Verification of Large Synthesized Designs. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), Seiten 534–537, 1993.

    Google Scholar 

  59. Turing, A.: On Computable Numbers With An Application To The Entscheidungs Problem. In: Proceedings of The London Mathematical Society, Band 42 der Reihe 2, Seiten 230–265, 1937.

    Google Scholar 

  60. Liggesmeyer, P.: Software-Qualität – Testen, Analysieren und Verifizieren von Software. Spektrum Akademischer Verlag, Heidelberg, Berlin, 2002.

    MATH  Google Scholar 

  61. Gajski, D. D. und R. H. Kuhn: New VLSI Tools. IEEE Computer, 16(12):11–14, 1983.

    Google Scholar 

  62. SystemC Verification Working Group: SystemC Verification Standard Specification, 2006. Version 1.0e, http://www.systemc.org.

  63. Kernighan, B. W. und D. Ritchie: The C Programming Language. Prentice-Hall, Inc., Upper Saddle River, NJ, U.S.A., 1988. 2. Auflage.

    Google Scholar 

  64. Gödel, Kurt: über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931.

    Google Scholar 

  65. IEEE: IEEE Standard Glossary of Software Engineering Terminology. IEEE Std 610.12-1990, 1990.

    Google Scholar 

  66. Strahm, T.: Logik in Informatik, Mathematik und Philosophie, 1999. Vortrag anlässlich der Veranstaltung Theodor-Kocher-Preis 1998 der Universität Bern.

    Google Scholar 

  67. Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.

    Article  MATH  Google Scholar 

  68. ITRS: International Technology Roadmap for Semiconductors – System Drivers. Technischer Bericht, ITRS, 2007. http://www.itrs.net/.

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Christian Haubelt .

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Haubelt, C., Teich, J. (2010). Einleitung. In: Digitale Hardware/Software-Systeme. eXamen.press, vol 0. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05356-6_1

Download citation

Publish with us

Policies and ethics