System-on-chip Verification project

Hardware verification group

Technical Report

SystemC is among a group of system level design languages proposed to raise the abstraction level for embedded system design and verification. Defining the formal semantics of SystemC is an important and mandatory step towards enabling the formal verification of SystemC. In this technical report, we present a sound and complete semantics of the main parts of SystemC in fixpoint. Such a semantics are a precise and non ambiguous definitions of the SystemC library. They are very useful to guarantee a unique implementation of the library and interpretation of its behaviour. Besides, they can used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages.

SystemC Semantics in Fixpoint

A. Habibi and S. Tahar

Date: December 2004

· Download PDF file: (PDF file)

· Send comments and suggestions to: habibi@ece.concordia.ca