An effective approach for model checking SystemC designs

SystemC is a system level modeling language with the goal of enabling verification at higher levels of abstraction. In this paper, we propose a mapping from SystemC designs to Rebeca models supported by an automatic tool, Sytra. Rebeca verification tool set is then available for verifying LTL and CTL properties. The mapping is aimed to preserve the concurrent and event-driven nature of SystemC. This work is part of a project (Sysfier) to formally verify SystemC designs. The applicability of our approach is shown by a set of small and medium sized case studies, and the scalability of the approach is shown by the verification of a single-cycle MIPS design.