Verifying SystemC using Intermediate Verification Language and Stateful Symbolic Simulation

Formal verification of high-level SystemC designs is an important and challenging problem. One has to deal with the full complexity of C++ to extract a suitable formal model (front-end problem) and then, with large cyclic state spaces defined by symbolic inputs and concurrent processes. This paper describes a scalable and efficient stateful symbolic simulation approach for SystemC that combines State Subsumption Reduction (SSR) with Partial Order Reduction (POR) and Symbolic Execution (SymEx) under the SystemC simulation semantics. While the SymEx+POR combination provides basic capabilities to efficiently explore the state space, SSR prevents revisiting symbolic states and therefore makes the verification complete. The approach has been implemented on top of an Intermediate Verification Language (IVL) for SystemC to address the front-end problem. The scalability and efficiency of the implemented verifier is demonstrated using an extensive set of experiments.