TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox

Leibniz Transactions on Embedded Systems

Claude Helmstetter¹ 

[1] Verimag - CNRS2 Avenue de Vignate, 38610 Gières, France;

关键词: Model checking;    Verification;    Simulation;    SystemC;    Transactional modeling;   

DOI  :  10.4230/LITES-v001-i001-a002

来源: DOAJ

【 摘 要 】

SystemC/TLM models, which are C++ programs, allow the simulation of embedded software before hardware low-level descriptions are available and are used as golden models for hardware verification. The verification of the SystemC/TLM models is an important issue since an error in the model can mislead the system designers or reveal an error in the specifications. An open-source simulator for SystemC/TLM is provided but there are no tools for formal verification.

In order to apply model checking to a SystemC/TLM model, a semantics for standard C++ code and for specific SystemC/TLM features must be provided. The usual approach relies on the translation of the SystemC/TLM code into a formal language for which a model checker is available.

We propose another approach that suppresses the error-prone translation effort. Given a SystemC/TLM program, the transitions are obtained by executing the original code using g++ and an extended SystemC library, and we ask the user to provide additional functions to store the current model state. These additional functions generally represent less than 20% of the size of the original model, and allow it to apply all CADP verification tools to the SystemC/TLM model itself.

【 授权许可】

Unknown