Affiliations: Ecole Polytechnique Fédérale de Lausanne, Station 14, CH-1015 Lausanne, Switzerland. [email protected] | Eindhoven University of Technology, P.O. Box 513, NL-5600MB, Eindhoven, The Netherlands. [email protected] | Reykjavik University, Reykjavik, Iceland, University of Tehran, Tehran, Iran. [email protected]
Note: [] Address for correspondence: Department of Computer Science, TU/Eindhoven, P.O. Box 513, Eindhoven, NL-5600MB, The Netherlands
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.
Keywords: SystemC, Process Algebra, Formal Verification, mCRL2
