Application of Process Algebraic Verification and Reduction Techniques to SystemC Designs
Hossein Hojjat, Mohammad Reza Mousavi, Marjan Sirjani · TU/e Research Portal · 2008
SystemC is an IEEE standard system-level language used in hardware/software codesign 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.