Date and Time:Monday, 21 January 2007, 15:30-ca. 16:30

Speaker:Hossein Hojjat

Title: Process Algebraic Verification of SystemC Codes.

Abstract:

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This presentation describes a formal approach to verifying SystemC codes by providing a mapping to the process algebra mCRL2.
The outstanding advantages of mCRL2 are the support for different data types and a powerful tool-set for model reduction and analysis. A tool is implemented to automatically perform the proposed mapping. We establish the applicability of our method by analyzing a number of practical case-studies, including verifying the data semantics of a MIPS processor specified in SystemC.
(joint work with Mohammad Mousavi and Marjan Sirjani)