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

https://hal.inria.fr/inria-00275456
Contributor : Olivier Ponsini <>
Submitted on : Wednesday, April 23, 2008 - 7:42:39 PM
Last modification on : Thursday, November 19, 2020 - 1:00:24 PM

Identifiers

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

Collections

Citation

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⟩

Share

Metrics

Record views

627