A Comparison of Two SystemC/TLM Semantics for Formal Verification - INRAE - Institut national de recherche pour l’agriculture, l’alimentation et l’environnement Access content directly
Conference Papers Year : 2008

A Comparison of Two SystemC/TLM Semantics for Formal Verification


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.
No file

Dates and versions

inria-00275456 , version 1 (23-04-2008)


  • 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⟩
218 View
0 Download


Gmail Facebook X LinkedIn More