Publications:Formal analysis of systemc designs in process algebra

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Formal analysis of systemc designs in process algebra
Author Hossein Hojjat and Mohammad Reza Mousavi and Marjan Sirjani
Year 2011
PublicationType Journal Paper
Journal Fundamenta Informaticae
Diva url
Abstract SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.