ESL Design and Verification

  • Frank RoginEmail author
  • Rolf Drechsler


First, the state-of-the-art of modeling and verification at the ESL is briefly summarized in this chapter. As SystemC has been developed as a de-facto standard for system level design over the past few years, it is used for practical demonstration purposes in this book. Next, the introduced ESL methodologies and techniques are discussed under the SystemC perspective. Finally, our systematic debugging approach for ESL designs is described.


Model Check Abstraction Level Formal Verification Single Instruction Multiple Data Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. ITRS07.
    International Technology Roadmap for Semiconductors - Design, ITRS Edition 2007. [Online], accessed January 2009.
  2. BMP07.
    B. Bailey, G. Martin, and A. Piziali. ESL Design and Verification: A Prescription for Electronic System Level Methodology. Morgan Kaufmann, 2007.Google Scholar
  3. GV+94.
    D.D. Gajski, F. Vahid, S. Narayan, and J. Gong. Specification and Design of Embedded Systems. Prentice Hall, Englewood Cliffs, NJ, 1994.zbMATHGoogle Scholar
  4. Kog06.
    T. Kogel. Peripheral Modeling for Platform Driven ESL Design. In PlatformBased Design at the Electronic System Level, pp. 71–85, Springer, 2006.CrossRefGoogle Scholar
  5. TH07.
    J. Teich and C. Haubelt. Digitale Hardware/Software-Systeme. 2.erweiterte Auflage, Springer-Verlag Berlin Heidelberg, 2007.zbMATHGoogle Scholar
  6. TLM2.
    TLM Working Group. OSCI TLM2 User Manual. In TLM2 documentation package, [Online],, accessed July 2008.
  7. FGP07.
    G. Fey and R. Drechsler. Improving Simulation-Based Verification by Means of Formal Methods. In Asia and South Pacific Design Automation Conference, pp. 640–643, 2004.Google Scholar
  8. Ash06.
    P. Ashenden. The Designer’s Guide to VHDL. Morgan Kaufmann, 3rd revised edition, 2006.Google Scholar
  9. Pal03.
    S. Palnitkar. Verilog HDL: A Guide to Digital Design and Synthesis. Prentice Hall, 2nd edition, 2003.Google Scholar
  10. IE+06.
    IEEE Computer Society. IEEE Standard SystemC Language Reference Manual. 2006.Google Scholar
  11. BDBK08.
    D. C. Black, J. Donovan, B. Bunton, and A. Keist. SystemC: From the Ground Up. Spinger, 2nd edition, 2008.Google Scholar
  12. Ghe06.
    H. Foster, A. Krolnik, and D. Lacey. Assertion-Based Design. Kluwer, 2003.CrossRefGoogle Scholar
  13. ARL00.
    D. Abts, M. Roberts, and D.J. Lilja. A Balanced Approach to High-level Verification: Performance Trade-offs in Verifying Large-scale Multiprocessors. In International Conference on Parallel Processing, pp. 505–510, 2000.Google Scholar
  14. Kro99.
    T. Kropf. Introduction to Formal Hardware Verification. Springer, 1999.zbMATHCrossRefGoogle Scholar
  15. WOLB92.
    L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. McGraw-Hill, 2nd edition, 1992.zbMATHGoogle Scholar
  16. KPKG02.
    A. Kuehlmann, V. Paruthi, F. Krohm, and M.K. Ganai. Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions in Computer-Aided Design, 21(12):1377–1394, 2002.CrossRefGoogle Scholar
  17. CGP00.
    E.M. Clarke, O. Grumberg, and D.A. Peled. Model checking. MIT Press, Cambridge, MA, 2000.Google Scholar
  18. Bra83.
    D. Brand. Redundancy and Don’t Cares in Logic Synthesis. IEEE Transactions on Computers, 32(10):947–952, 1983.MathSciNetzbMATHCrossRefGoogle Scholar
  19. BB+07.
    J. Bormann, S. Beyer, A. Maggiore, M. Siegel, S. Skalberg, T. Blackmore, and F. Bruno. Complete Formal Verification of TriCore2 and Other Processors. In DVCon, 2007.Google Scholar
  20. NOT06.
    R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM, 53(6):937–977, 2006.MathSciNetCrossRefGoogle Scholar
  21. FKL03.
    M. Fujita, I. Gosh, and M. Prasad. Verification Techniques for System-Level Design. Morgan Kaufmann Series in Systems on Silicon, 2007.Google Scholar
  22. IE+05a.
    IEEE Computer Society. IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language. 2005.Google Scholar
  23. IE+05b.
    IEEE Computer Society. IEEE Standard for Property Specification Language. 2005.Google Scholar
  24. OVL.
    Accellera Organization. Accellera Standard OVL V2. [Online], accessed April 2008.
  25. YPA06.
    J. Yuan, C. Pixley, and A. Aziz. Constraint-Based Verification. Springer, 2006.zbMATHGoogle Scholar
  26. SCV.
    SystemC Verification Group. SystemC Verification Standard Specification - Version 1.0e. [Online], accessed November 2008.
  27. GED07.
    D. Große, R. Ebendt, and R. Drechsler. Improvements for Constraint Solving in the SystemC Verification Library. In Great Lakes Symposium on VLSI, pp. 493–496, 2007.Google Scholar
  28. GWSD08.
    D. Große, R. Wille, R. Siegmund, and R. Drechsler. Contradiction Analysis for Constraint-Based Random Simulation. In Forum on Specification & Design Languages, pp. 130–135, 2008.Google Scholar
  29. SMA04.
    K. R.G. da Silva, E. U.K. Melcher, and G. Araujo. An Automatic Testbench Generation tool for a SystemC Functional Verification Methodology. In Symposium on Integrated Circuits and System Design, pp. 66–70, 2004.Google Scholar
  30. PC05.
    S. Park and S. Chae. A C/C++-Based Functional Verification Framework Using the SystemC Verification Library. In IEEE International Workshop on Rapid System Prototyping, pp. 237–239, 2005.Google Scholar
  31. GCOV.
    F. Ghenassia. Transaction-Level Modeling with SystemC. Kluwer Academic Publishers, 2006.Google Scholar
  32. GPKD08.
    D. Große, H. Peraza, W. Klingauf, and R. Drechsler. Measuring the Quality of a SystemC Testbench by Using Code Coverage Techniques. In Embedded Systems Specification and Design Languages: Selected Contributions from FDL’07, pp. 73-86, Springer, 2008.CrossRefGoogle Scholar
  33. RHKR01.
    J. Ruf, D.W. Hoffmann, T. Kropf, and W. Rosenstiel. Simulation-Guided Property Checking on Multi-Valued AR-Automata. In Design, Automation and Test in Europe, pp. 742–748, 2001.Google Scholar
  34. HT04.
    A. Habibi and S. Tahar. On the Extension of SystemC by SystemVerilog Assertions. In Canadian Conference on Electrical and Computer Engineering, Volume: 4, pp. 1869–1872, 2004.Google Scholar
  35. HT06.
    A. Habibi and S. Tahar. Design and Verification of SystemC Transaction-Level Models. IEEE Transactions on VLSI Systems, 14(1):57–68, 2006.CrossRefGoogle Scholar
  36. GD04a.
    D. Große and R. Drechsler. Checkers for SystemC Designs. In International Conference on Formal Methods and Models for Codesign, pp. 171–178, 2004.Google Scholar
  37. BFF05.
    N. Bombieri, A. Fedeli, and F. Fummi. On PSL Properties Re-use in SoC Design Flow Based on Transaction Level Modeling. In International Workshop on Microprocessor Test and Verification, pp. 127–132, 2005.Google Scholar
  38. DG+05.
    A. Dahan, D. Geist, L. Gluhovsky, D. Pidan, G. Shapir, Y. Wolfsthal, L. Benalycherif, R. Kamidem, and Y. Lahbib. Combining System Level Modeling with Assertion based Verification. In International Symposium on Quality of Electronic Design, pp. 310–315, 2005.Google Scholar
  39. NH06.
    B. Niemann and C. Haubelt. Assertion-Based Verification of Transaction Level Models. In Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, pp. 232–236, 2006.Google Scholar
  40. SLU05.
    O. Spinczyk, D. Lohmann, and M. Urban, AspectC++: an AOP Extension for C++. Software Developer’s Journal, pp. 68–76, 2005.Google Scholar
  41. KT07.
    A. Kasuya and T. Tesfaye. Verification Methodologies in a TLM-to-RTL Design Flow. In Design Automation Conference, pp. 199–204, 2007.Google Scholar
  42. MR+01.
    W. Mueller, J. Ruf, D. Hoffmann, J. Gerlach, T. Kropf, and W. Rosenstiehl. The Simulation Semantics of SystemC. In Design, Automation and Test in Europe, pp. 64–70, 2001.Google Scholar
  43. HT05.
    A. Habibi and S. Tahar. On the Transformation of SystemC to AsmL Using Abstract Interpretation. Electronic Notes in Theoretical Computer Science, Vol. 131:39–49, 2005.CrossRefGoogle Scholar
  44. Sal03.
    A. Salem. Formal Semantics of Synchronous SystemC. In Design, Automation and Test in Europe, pp. 376–381, 2003.Google Scholar
  45. DG02.
    GNU test coverage program gcov. [Online], accessed June 2008.
  46. GD03.
    P. Godefroid. Model checking for programming languages using VeriSoft. In Symposium on Principles of Programming Languages, pp. 174–186, 1997.Google Scholar
  47. KS05.
    D. Kröning and N. Sharygina. Formal Verification of SystemC by Automatic Hardware/Software Partitioning. In Conference on Formal Methods and Programming Models for Codesign, pp. 101–110, 2005.Google Scholar
  48. OHT04.
    K. Oumalou, A. Habibi, and S. Tahar. Design for verification of a PCI bus in SystemC. In International Symposium on System-on-Chip, pp. 201–204,2004.Google Scholar
  49. MMM05a.
    M. Moy, F. Maraninchi, and L. Maillet-Contoz. LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. In International Conference on Application of Concurrency to System Design, pp. 26–35, 2005.Google Scholar
  50. HFG08.
    P. Herber, J. Fellmuth, and S. Glesner. Model Checking SystemC Designs Using Timed Automata. In International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 131–136, 2008.Google Scholar
  51. Zel05.
    A. Zeller. WHY PROGRAMS FAIL - A Guide to Systematic Debugging. Morgan Kaufmann, 2005.Google Scholar
  52. ZH02.
    A. Zeller and R. Hildebrandt. Simplifying and Isolating Failure-inducing Input. IEEE Transactions on Software Engineering, 28(2):183–200, 2002.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Institutsteil EntwurfsautomatisierungFraunhofer - Institut für Integrierte SchaltungenDresdenGermany
  2. 2.Universität Bremen AG RechnerarchitekturBremenGermany

Personalised recommendations