A Comparison of Two SystemC/TLM Semantics for Formal Verification

Claude Helmstetter and Olivier Ponsini

Proceedings of the 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE'2008 (Anaheim, USA), June 2008

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

10 pages

PDF

PostScript

Slides of O. Ponsini's lecture at MEMOCODE'08

PDF