TLM.OPEN: a SystemC/TLM Front-End for the CADP Verification Toolbox

Claude Helmstetter

Proceedings of the Workshop on Simulation Based Development of Certified Embedded Systems SBDCES'09 (Awaji Island, Hyogo, Japan), October 2009

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 verification 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 original model, and allow to apply all CADP tools to the SystemC/TLM program itself.

9 pages

PDF

PostScript