HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

A Comparison of Two SystemC/TLM Semantics for Formal Verification

Claude Helmstetter 1, 2 Olivier Ponsini 3
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
3 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The development of complex systems mixing hardware and software starts more and more by the design of functional models written in SystemC/TLM. These models are used as golden models for embedded software validation and for hardware verification, therefore their own validation is an important issue. One thriving approach consists in describing the semantics of SystemC/TLM in a formal language for which a verification tool exists. In this paper, we use LOTOS and the CADP toolbox as a unifying framework to define and experiment with two possible semantics for untimed SystemC/TLM, emphasizing either the nonpreemptive semantics of SystemC or the concurrent one of TLM. We also discuss and illustrate on a benchmark the qualitative versus quantitative performance trade-off offered by each semantics as regards verification. When associated with locks, our concurrent semantics appears both to provide more flexibility and to improve the scalability.
Complete list of metadata

Contributor : Olivier Ponsini Connect in order to contact the contributor
Submitted on : Wednesday, April 23, 2008 - 7:42:39 PM
Last modification on : Thursday, February 3, 2022 - 11:14:53 AM


  • HAL Id : inria-00275456, version 1
  • PRODINRA : 250085



Claude Helmstetter, Olivier Ponsini. A Comparison of Two SystemC/TLM Semantics for Formal Verification. Formal Methods and Models for Codesign (MEMOCODE), Jun 2008, Anaheim, United States. ⟨inria-00275456⟩



Record views