Skip to Main content Skip to Navigation
Conference papers

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS

Olivier Ponsini 1 Wendelin Serwe 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG [2007-2015] - Laboratoire d'Informatique de Grenoble [2007-2015]
Abstract : TLM (Transaction-Level Modeling) was introduced to cope with the increasing complexity of Systems-on-Chip designs by raising the modeling level. Currently, TLM is primarily used for system-level functional testing and simulation using the SystemC C++ API widely accepted in industry. Nevertheless, TLM requires a careful handling of asynchronous concurrency. In this paper, we give a semantics to TLM models written in SystemC via a translation into the process algebra LOTOS, enabling the verification of the models with the CADP toolbox dedicated to asynchronous systems. Contrary to other works on formal verification of TLM models written in SystemC, our approach targets fully asynchronous TLM without the restrictions imposed by the SystemC simulation semantics. We argue that this approach leads to more dependable models.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00259944
Contributor : Wendelin Serwe <>
Submitted on : Friday, February 29, 2008 - 6:10:53 PM
Last modification on : Friday, July 17, 2020 - 11:10:25 AM
Long-term archiving on: : Thursday, May 20, 2010 - 11:47:36 PM

File

Ponsini-Serwe-08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00259944, version 1

Collections

Citation

Olivier Ponsini, Wendelin Serwe. A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS. Formal Methods, May 2008, Turku, Finland. ⟨inria-00259944⟩

Share

Metrics

Record views

386

Files downloads

362