Verifying SystemC using an Intermediate Verification Language and Symbolic Simulation∗

Formal verification of SystemC is challenging. Before deal-ing with symbolic inputs and the concurrency semantics, a front-end is required to translate the design to a formal model. The lack of such front-ends has hampered the devel-opment of efficient back-ends so far. In this paper, we propose an isolated approach by using an Intermediate Verification Language (IVL). This enables a SystemC-to-IVL translator (frond-end) and an IVL veri-fier (back-end) to be developed independently. We present a compact but general IVL that together with an extensive benchmark set will facilitate future research. Furthermore, we propose an efficient symbolic simulator integrating Partial Order Reduction. Experimental compar-ison with existing approaches has shown its potential. 1