Document Open Access Logo

TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox

Author Claude Helmstetter

PDF
Thumbnail PDF

File

LITES-v001-i001-a002.pdf
  • Filesize: 0.71 MB
  • 18 pages

Document Identifiers

Author Details

Claude Helmstetter
  • Verimag - CNRS, 2 Avenue de Vignate, 38610 Gières, France

Cite AsGet BibTex

Claude Helmstetter. TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox. In LITES, Volume 1, Issue 1 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 1, pp. 02:1-02:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LITES-v001-i001-a002

Abstract

SystemC/TLM models, which are C++ programs, allow the simulation of embedded software before hardware low-level descriptions are available and are used as golden models for hardware verification. The verification of the SystemC/TLM models is an important issue since an error in the model can mislead the system designers or reveal an error in the specifications. An open-source simulator for SystemC/TLM is provided but there are no tools for formal verification.In order to apply model checking to a SystemC/TLM model, a semantics for standard C++ code and for specific SystemC/TLM features must be provided. The usual approach relies on the translation of the SystemC/TLM code into a formal language for which a model checker is available.We propose another approach that suppresses the error-prone translation effort. Given a SystemC/TLM program, the transitions are obtained by executing the original code using g++ and an extended SystemC library, and we ask the user to provide additional functions to store the current model state. These additional functions generally represent less than 20% of the size of the original model, and allow it to apply all CADP verification tools to the SystemC/TLM model itself.

Subject Classification

ACM Subject Classification
  • Hardware
  • Hardware → Hardware validation
  • Hardware → Functional verification
  • Hardware → Transaction-level verification
Keywords
  • Model checking
  • Verification
  • Simulation
  • SystemC
  • Transactional modeling

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Accellera Systems Initiative. IEEE 1666 Standard: SystemC Language Reference Manual., 2011. URL: http://www.accellera.org.
  2. Nicolas Blanc and Daniel Kroening. Race analysis for SystemC using model checking. In 2008 International Conference on Computer-Aided Design (ICCAD’08), November 10–13, 2008, San Jose, CA, USA, pages 356–363. IEEE, 2008. URL: http://doi.acm.org/10.1145/1509456.1509540.
  3. Alessandro Cimatti, Iman Narasamdya, and Marco Roveri. Software model checking SystemC. IEEE Trans. on CAD of Integrated Circuits and Systems, 32(5):774–787, 2013. URL: https://doi.org/10.1109/TCAD.2012.2232351
  4. Rolf Drechsler and Daniel Große. Reachability analysis for formal verification of SystemC. In 2002 Euromicro Symposium on Digital Systems Design (DSD 2002), Systems-on-Chip, 4–6 September 2002, Dortmund, Germany, pages 337–340. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/DSD.2002.1115387
  5. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12–14, 2005, pages 110–121.ACM, 2005. URL: https://doi.org/10.1145/1040305.1040315
  6. Hubert Garavel. Open/cæsar: An OPen software architecture for verification, simulation, and testing. In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 – April 4, 1998, Proceedings, pages 68–84. Springer,1998. Full version available as INRIA Research Report RR-3352. URL: https://doi.org/10.1007/BFb0054165
  7. Hubert Garavel, Claude Helmstetter, Olivier Ponsini, and Wendelin Serwe. Verification of an industrial SystemC/TLM model using LOTOS and CADP. In 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), July 13–15, 2009, Cambridge, Massachusetts, USA, pages 46–55. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/MEMCOD.2009.5185377
  8. Hubert Garavel, Frédéric Lang, and Radu Mateescu. An overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter, 4:13–24, August 2002. Also available as INRIA Technical Report RT-0254 (December 2001). Google Scholar
  9. Hubert Garavel, Radu Mateescu, Frédéric Lang, and Wendelin Serwe. CADP 2006: A toolbox for the construction and analysis of distributed processes. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3–7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 158–163. Springer, July 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_18
  10. Frank Ghenassia, editor. Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems. Springer, June 2005. ISBN 0-387-26232-6. Google Scholar
  11. Daniel Große and Rolf Drechsler. CheckSyC: an efficient property checker for RTL SystemC designs. In International Symposium on Circuits and Systems (ISCAS 2005), 23–26 May 2005, Kobe, Japan, volume 4, pages 4167–4170. IEEE, May 2005. URL: https://doi.org/10.1109/ISCAS.2005.1465549
  12. Daniel Große, Hoang M. Le, and Rolf Drechsler. Proving transaction and system-level properties of untimed SystemC TLM designs. In 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), Grenoble, France, 26–28 July 2010, pages 113–122. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/MEMCOD.2010.5558643
  13. Claude Helmstetter. Validation de modèles de systèmes sur puce en présence d’ordonnancements indéterministes et de temps imprécis. PhD thesis, INPG, Grenoble, France, March 2007. URL: http://tel.archives-ouvertes.fr/tel-00350929.
  14. Claude Helmstetter, Florence Maraninchi, and Laurent Maillet-Contoz. Test coverage for loose timing annotations. In Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26– 27, and August 31, 2006, Revised Selected Papers, volume 4346, pages 100–115. Springer, August 2006. URL: https://doi.org/10.1007/978-3-540-70952-7_7
  15. Claude Helmstetter, Florence Maraninchi, and Laurent Maillet-Contoz. Full simulation coverage for SystemC transaction-level models of systems-on-a-chip. Formal Methods in System Design, 35(2):152–189, 2009. URL: https://doi.org/10.1007/s10703-009-0075-z
  16. Claude Helmstetter and Olivier Ponsini. A comparison of two SystemC/TLM semantics for formal verification. In 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), June 5–7, 2008, Anaheim, CA, USA, pages 59–68. IEEE Computer Society, June 2008. URL: https://doi.org/10.1109/MEMCOD.2008.4547687
  17. Paula Herber, Marcel Pockrandt, and Sabine Glesner. Transforming SystemC transaction level models into UPPAAL timed automata. In 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11–13 July, 2011, pages 161–170. IEEE, 2011. URL: https://doi.org/10.1109/MEMCOD.2011.5970523
  18. ISO/IEC. Lotos – a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, International Organization for Standardization – Information Processing Systems – Open Systems Interconnection, Genève, September 1989. Google Scholar
  19. Vania Joloboff and Claude Helmstetter. SimSoC: A SystemC TLM integrated ISS for full system simulation. In Circuits and Systems, 2008. APCCAS 2008. IEEE Asia Pacific Conference on. IEEE, 2008. URL: https://doi.org/10.1109/APCCAS.2008.4746381
  20. Daniel Kroening and Natasha Sharygina. Formal verification of SystemC by automatic hardware/software partitioning. In 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 11–14 July 2005, Verona, Italy, Proceedings, pages 101–110. IEEE, 2005. URL: https://doi.org/10.1109/MEMCOD.2005.1487900
  21. Sudipta Kundu, Malay K. Ganai, and Rajesh Gupta. Partial order reduction for scalable testing of SystemC TLM designs. In Proceedings of the 45th Design Automation Conference, DAC 2008, Anaheim, CA, USA, June 8–13, 2008, pages 936– 941. ACM, 2008. URL: https://doi.org/10.1145/1391469.1391706
  22. Kevin Marquet, Matthieu Moy, and Bertrand Jeannet. Efficient Encoding of SystemC/TLM in Promela. In Workshop on Design, Analysis and Tools for Integrated Circuits and Systems at the International MultiConference of Engineers and Computer Scientists 2011, DATICS-IMECS, pages 1039–1044, 2011. URL: http://www.iaeng.org/publication/IMECS2011/ IMECS2011_pp1039-1044.pdf.
  23. Matthieu Moy. Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level. PhD thesis, INPG, Grenoble, France, December 2005. URL: http://www-verimag.imag. fr/~moy/phd/.
  24. Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 10(2–3):73–104, 2005. URL: https://doi.org/10.1007/s10617-006-9044-6
  25. Bernhard Niemann and Christian Haubelt. Formalizing TLM with communicating state machines. In Forum on specification and Design Languages, FDL 2006, September 19–22, 2006, Darmstadt, Germany, Proceedings, pages 285–293. ECSI, 2006. Google Scholar
  26. Olivier Ponsini and Wendelin Serwe. A schedulerless semantics of TLM models written in SystemC via translation into LOTOS. In FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26–30, 2008, Proceedings, volume 5014 of Lecture Notes in Computer Science, pages 278–293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68237-0_20
  27. Claus Traulsen, Jérôme Cornet, Matthieu Moy, and Florence Maraninchi. A SystemC/TLM semantics in Promela and its possible applications. In Model Checking Software, 14th International SPIN Workshop, Berlin, Germany, July 1–3, 2007, Proceedings, volume 4595 of Lecture Notes in Computer Science, pages 204–222. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73370-6_14
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact