Verifying SystemC using Stateful Symbolic Simulation∗

Formal verification of high-level SystemC designs is an im-portant and challenging problem. Recent works have pro-posed symbolic simulation in combination with Partial Or-der Reduction (POR) as a promising solution and experi-mentally demonstrated its potential. However, these sym-bolic simulation approaches have a fundamental limitation in handling cyclic state spaces. The reason is that they are based on stateless model checking and thus unable to avoid revisiting states in a cycle. In this paper, we propose a novel stateful symbolic simulation approach for SystemC. For the efficient detection of revisited symbolic states, we apply sym-bolic subsumption checking. Furthermore, our implementa-tion integrates a cycle proviso to preserve the soundness of POR in the presence of cycles. We demonstrate the scala-bility and the efficiency of the proposed approach using an extensive set of experiments. 1