A Symbolic Partial Order Method for Verifying SystemC

SystemC is an IEEE standard system-level language and has been widely adopted in development of embedded systems. Verifying SystemC designs is critical since it can avoid error propagation down to the final implementation. Recent works translate SystemC designs into transition systems and verify them by model checking. However, model checking suffers from the state space explosion problem. This work combines partial order reduction and symbolic model checking to combating state space explosion in verifying SystemC. Some concepts are defined to assisting in partial order reduction according to the characteristics of SystemC transition systems, and partial order reduction algorithms for symbolic model checking are presented based on these concepts. Our approach is implemented on symbolic model checker VERDS and the efficiency is demonstrated by verifying a set of SystemC designs.