Database of Research Tools Developed Using CADP

TLM.open: A SystemC/TLM Front-End for CADP

Organisation: LACL, Université Paris-Est, Paris (FRANCE)
Inria Grenoble Rhône-Alpes and LIG, Grenoble (FRANCE)

Functionality: Implementation of the OPEN/CAESAR API for SystemC/TLM

Tools used: CADP (Construction and Analysis of Distributed Processes)
OSCI SystemC simulator

Period: 2009

Description: SystemC/TLM models are often used for the simulation of an embedded software before the hardware RTL descriptions are available, and as golden models for hardware verification. Thus, the verification of the SystemC/TLM models themselves is important. However, although the OSCI (Open SystemC Initiative) provides an open-source simulator for SystemC/TLM and a C++ library to ease test generation, OSCI does not provide tools for formal verification.

In order to apply model checking to a SystemC/TLM program, the usual approach relies on the translation of the SystemC/TLM code to a formal language for which a model checker is available. TLM.OPEN avoids this translation, and executes the transitions of the model using a C++ compiler (e.g., g++) and the OSCI library, relying on user-provided functions to store the current program state. These additional functions represent generally less than 20% of the size of the original model.

Conclusions: TLM.open enables the application of CADP to check complex properties of SystemC/TLM models. Using TLM.open is simpler than using manual translations and scales up better than previous work. Thanks to the numerous tools of CADP, it is now possible to check complex properties, and to test the equivalence of two SystemC/TLM programs

Publications: [Helmstetter-09] Claude Helmstetter. "TLM.open: a SystemC/TLM Front-end for the CADP Verification Toolbox". Extended abstract. Workshop on Simulation Based Development of Certified Embedded Systems SBDCES'09 (Awaji Island, Hyogo, Japan), October 2009.
Available on-line at: http://hal.inria.fr/hal-00429070/en
or from the CADP Web site in PDF or PostScript

[Helmstetter-14] Claude Helmstetter. "TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox". Leibniz Transactions on Embedded Systems 1(1), pp. 02:1-02:18, April 2014.
Available on-line at: http://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v001-i001-a002
or from the CADP Web site in PDF or PostScript

Contact:
Claude Helmstetter
Inria Grenoble Rhône Alpes / VASY project-team
655, avenue de l'Europe
38330 Montbonnot
FRANCE
E-mail: Claude.Helmstetter@inria.fr



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Thu Feb 11 12:23:11 2021.


Back to the CADP research tools page