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, ...
Complete list of metadatas
Contributor : Claude Helmstetter <>
Submitted on : Friday, October 30, 2009 - 5:03:17 PM
Last modification on : Friday, October 12, 2018 - 1:18:14 AM
Long-term archiving on : 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. 2009. ⟨hal-00429070⟩



Record views


Files downloads