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

Claude Helmstetter 1, *
* Corresponding author
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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.
Document type :
Preprints, Working Papers, ...
Extended abstract for SBDCES workshop ( 2009
Liste complète des métadonnées
Contributor : Claude Helmstetter <>
Submitted on : Friday, October 30, 2009 - 5:03:17 PM
Last modification on : Saturday, October 31, 2009 - 9:44:29 AM
Document(s) archivé(s) le : Tuesday, October 16, 2012 - 1:01:35 PM


Files produced by the author(s)


  • HAL Id : hal-00429070, version 1



Claude Helmstetter. a SystemC/TLM Front-end for the CADP Verification Toolbox. Extended abstract for SBDCES workshop ( 2009. <hal-00429070>



Record views


Document downloads