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.
Type de document :
Communication dans un congrès
Formal Methods and Models for Codesign (MEMOCODE), Jun 2008, Anaheim, United States. 2008
Liste complète des métadonnées

https://hal.inria.fr/inria-00275456
Contributeur : Olivier Ponsini <>
Soumis le : mercredi 23 avril 2008 - 19:42:39
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Identifiants

  • HAL Id : inria-00275456, version 1

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. 2008. 〈inria-00275456〉

Partager

Métriques

Consultations de la notice

361