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

Back to the CADP research tools page