Hojjat, HosseinMousavi, Mohammad RezaSirjani, Marjan2011-12-162011-12-162011-12-16201110.3233/FI-2011-391https://infoscience.epfl.ch/handle/20.500.14299/73590WOS:000294729300002SystemC 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.SystemCProcess AlgebraFormal VerificationmCRL2VerificationAsmltext::journal::journal article::research article