Verifying SystemC using stateful symbolic simulation

Formal verification of high-level SystemC designs is an important and challenging problem. Recent works have proposed symbolic simulation in combination with Partial Order Reduction (POR) as a promising solution and experimentally demonstrated its potential. However, these symbolic 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 symbolic subsumption checking. Furthermore, our implementation integrates a cycle proviso to preserve the soundness of POR in the presence of cycles. We demonstrate the scalability and the efficiency of the proposed approach using an extensive set of experiments.