Model checking SystemC designs using timed automata

ABSTRACT

SystemC is widely used for modeling and simulation in hardware/software co-design. Due to the lack of a complete formal semantics, it is not possible to verify SystemC designs. In this paper, we present an approach to overcome this problem by defining the semantics of SystemC by a mapping from SystemC designs into the well-defined semantics of Uppaal timed automata. The informally defined behavior and the structure of SystemC designs are completely preserved in the generated Uppaal models. The resulting Uppaal models allow us to use the Uppaal model checker and the Uppaal tool suite, including simulation and visualization tools. The model checker can be used to verify important properties such as liveness, deadlock freedom or compliance with timing constraints. We have implemented the presented transformation, applied it to two examples and verified liveness, safety and timing properties by model checking, thus showing the applicability of our approach in practice.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: G. Behrmann, A. David, and K. G. Larsen. A Tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems, LNCS 3185. Springer, 2004.
• 3: Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi, UPPAAL—a tool suite for automatic verification of real-time systems, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.232-243, July 1996, New Brunswick, NeW Jersey, United States
• 4: J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. In Lecture Notes on Concurrency and Petri Nets, LNCS 3098. Springer, 2004.
• 5: FZI Research Center for Information Technology. KaSCPar - Karlsruhe SystemC Parser Suite.
• 6: Thorsten Grotker, System Design with SystemC, Kluwer Academic Publishers, Norwell, MA, 2002
• 7: D. Grosse and R. Drechsler. Checkers for SystemC designs. In Formal Methods and Models for Codesign, pages 171--178, 2004.
• 8: Daniel Groβe , Ulrich Kühne , Rolf Drechsler, HW/SW co-verification of embedded systems using bounded model checking, Proceedings of the 16th ACM Great Lakes symposium on VLSI, April 30-May 01, 2006, Philadelphia, PA, USA [doi>10.1145/1127908.1127920]
• 9: Ali Habibi , Haja Moinudeen , Sofiène Tahar, Generating finite state machines from SystemC, Proceedings of the conference on Design, automation and test in Europe: Designers' forum, March 06-10, 2006, Munich, Germany
• 10: A. Habibi and S. Tahar. An Approach for the Verification of SystemC Designs Using AsmL. In Automated Technology for Verification and Analysis, pages 69--83, 2005.
• 11: IEEE Standards Association. IEEE Std. 1666--2005, Open SystemC Language Reference Manual, 2005.
• 12: Daniel Karlsson , Petru Eles , Zebo Peng, Formal verification of systemc designs using a petri-net based representation, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 13: K. Man. An Overview of SystemCFL. In Research in Microelectronics and Electronics, volume 1, 2005.
• 14: K. L. Man, A. Fedeli, M. Mercaldi, M. Boubekeur, and M. P. Schellekens. SC2SCFL: Automated SystemC to SystemCFL Translation. In Embedded Computing Systems: Architectures, Modeling, and Simulation, LNCS 4599, pages 34--45. Springer, 2007.
• 15: Wolfgang Müller , Jürgen Ruf , Wolfgang Rosenstiel, An ASM based systemC simulation semantics, SystemC: methodologies and applications, Kluwer Academic Publishers, Norwell, MA, 2003
• 16: J. Ruf , D. Hoffmann , J. Gerlach , T. Kropf , W. Rosenstiehl , W. Mueller, The simulation semantics of systemC, Proceedings of the conference on Design, automation and test in Europe, p.64-70, March 2001, Munich, Germany
• 17: Ashraf Salem, Formal Semantics of Synchronous SystemC, Proceedings of the conference on Design, Automation and Test in Europe, p.10376, March 03-07, 2003

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Verification

Keywords:
SystemC, model checking, timed automata