TLM.open: a SystemC/TLM Front-end for the CADP Verification Toolbox

Claude Helmstetter (1)

1 VASY - System validation - Research and applications

SystemC/TLM models allow the simulation of the embedded software before the hardware RTL descriptions are available, and are used as golden models for hardware verification. The verifi- cation of the SystemC/TLM models is an important issue, since a error in the model can mislead the system designers, or reveal an error in the specification. The OSCI provides an open-source simulator for SystemC/TLM but no 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. We propose another approach that suppress the error-prone translation effort. Given a SystemC/TLM program, we execute the transitions using g++ and the OSCI library, and we ask the user to provide additional functions to store the current program state. These additional functions represent generally less than 20% of the size of the origianl model, and allows to apply all CADP tools to the SystemC/TLM program itself.

Mots clés: Transactional Modeling; Embedded Systems; Model checking

Domaines: Systèmes embarqués; Modélisation et simulation

Claude Helmstetter. TLM.open: a SystemC/TLM Front-end for the CADP Verification Toolbox. 2009. ⟨hal-00429070⟩