access icon free System-level assertions: approach for electronic system-level verification

As design of digital systems become more complex and more transistors are incorporated into a single chip, design and verification methodologies moves into higher levels. Now that design at the register transfer level (RTL) has reached its maturity, the focus is shifting to electronic system level (ESL) design tools, languages and methodologies. At the centre of this and perhaps the most challenging are verification methods and tools to use for verifying designs at the ESL. This study presents a new concept of system-level assertions for ESL verification. It also demonstrates an environment for functionally verifying system-level designs using these system-level assertions. The proposed environment adapts existing EDA simulation tools, which are mainly used for RTL design and verification, and utilises them for system-level verification. In this environment, designs are modelled in SystemC-transaction level modelling 2.0, and assertions are written in SystemVerilog. Design and verification parts are connected together using SystemVerilog Direct Programming Interface mechanism, and designs that are described in SystemC are verified against system-level assertions in the course of SystemVerilog simulation.

Inspec keywords: formal verification; electronic engineering computing; C language

Other keywords: SystemC-transaction level modelling 2.0; EDA simulation tools; electronic system-level verification; system-level assertion; ESL verification; electronic system level design tools; SystemVerilog direct programming interface mechanism

Subjects: Formal methods; Electronic engineering computing

References

    1. 1)
      • 22. Tabakov, D., Vardi, M., Kamhi, G., Singerman, E.: ‘A temporal language for SystemC’. FMCAD, 2008, pp. 19.
    2. 2)
      • 1. IEEE Standard SystemC Language Reference Manual, IEEE Standard 1666-2011, 2011, DOI = http://www.accellera.org.
    3. 3)
      • 16. Ecker, W., Esen, V., Steininger, T., Velten, M., Hull, M.: ‘Specification language for transaction level assertions’. HLDVT, 2006, pp. 7784.
    4. 4)
      • 18. Ferro, L., Pierre, L.: ‘ISIS: runtime verification of TLM platforms’. FDL, 2009, pp. 16.
    5. 5)
      • 7. Vardi, M.Y.: ‘Formal techniques for SystemC verification’. DAC, 2007, pp. 188192.
    6. 6)
      • 13. Kallel, M., Lahbib, Y., Tourki, R., Baganne, A.: ‘Verification of SystemC transaction level models using an aspect-oriented and generic approach’. DTIS, 2010, pp. 16.
    7. 7)
      • 12. Niemann, B., Haubelt, C.: ‘Assertion-based verification of transaction level models’. ITG/GI/GMM Workshop, 2006, pp. 232236.
    8. 8)
      • 14. Endoh, Y.: ‘ASystemC: an AOP extension for hardware description Language’. Aspect-Oriented Software Development, 2011, pp. 1928.
    9. 9)
      • 5. IEEE Standard for SystemVerilog: Unified Hardware Design, Specification, and Verification Language, IEEE Standard 1800, 2012.
    10. 10)
      • 26. Erickson, A.: ‘Introducing UVM connect’, Mentor Graphics Verif. Horiz., 2012, 8, (1), pp. 612.
    11. 11)
      • 21. Jeda Technologies Inc.: JEDA TLM 2.0 Validation Suite, DOI = http://www.jedatechnologies.net.
    12. 12)
      • 25. Universal Verification Methodology (UVM), 2013, DOI = http://www.accellera.org.
    13. 13)
      • 6. The 2012 Wilson Research Group Functional Verification Study, Mentor Graphics, DOI = http://www.blogs.mentor.com/verificationhorizons/blog/2013/08/12/part-9-the-2012-wilson-research-group-functional-verification-study/.
    14. 14)
      • 24. Chen, M., Mishra, P.: ‘Assertion-based functional consistency checking between TLM and RTL models’. VLSID, 2013, pp. 320325.
    15. 15)
      • 3. Accellera Standard OVL V2 Reference Manual, Accellera Systems Initiative, 2013.
    16. 16)
      • 23. Bombieri, N., Fummi, F., Pravadelli, G.: ‘On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL’. DATE, 2006, pp. 16.
    17. 17)
      • 10. Große, D., Drechsler, R.: ‘Checkers for SystemC designs’. Formal Methods and Models for Co-Design, 2004, pp. 171178.
    18. 18)
      • 28. Mentor Graphics ModelSim, DOI = http://www.mentor.com/products/fv/modelsim.
    19. 19)
      • 27. Smith, D.: ‘Asynchronous behaviors meet their match with SystemVerilog assertions’. DVCON, 2010.
    20. 20)
      • 15. Tabakov, D., Vardi, M.Y.: ‘Automatic aspectization of SystemC’. MISS, 2012, pp. 914.
    21. 21)
      • 17. Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: ‘A SystemC/TLM semantics in Promela and its possible applications’. Model Checking Software, 2007, pp. 204222.
    22. 22)
    23. 23)
      • 4. IEEE Standard for Property Specification Language (PSL), IEEE Standard 1850-2010, 2010.
    24. 24)
      • 20. Kasuya, A., Tesfaye, T.: ‘Verification methodologies in a TLM-to-RTL design flow’. DAC, 2007, pp. 199204.
    25. 25)
      • 8. Karlsson, D., Eles, P., Peng, Z.: ‘Formal verification of SystemC designs using a Petri-net based representation’. DATE, 2006, pp. 12281233.
    26. 26)
    27. 27)
      • 19. Ferro, L., Pierre, L.: ‘Formal semantics for PSL modeling layer and application to the verification of transactional models’. DATE, 2010, pp. 12071212.
    28. 28)
      • 2. International Technology Roadmap for Semiconductors (ITRS) – Design, 2011, DOI = http://www.itrs.net/Links/2011ITRS/Home2011.htm.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cdt.2014.0084
Loading

Related content

content/journals/10.1049/iet-cdt.2014.0084
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading