Formal Deadlock Checking on High-Level SystemC Designs

One of the main purposes to use SystemC in system development is to perform system-level verification in the early design stage. However, simulation is still by far the only available solution for the high-level SystemC design verification. Nonetheless, traditional formal verification techniques, which rely on the translation of designs under verification to logic netlists, cannot be easily adopted here due to the concurrent/asynchronous nature and the abundant synthesis flexibilities of the high-level designs. In this paper, we propose a multi-layer modeling to represent the high-level SystemC designs. By representing the different aspects of the design with different structures - simulation kernel, predictive synchronization dependence graph (PSDG), and extended Petri net (extPN), our modeling can be very concise and faithfully capture the original design semantics. We develop a formal verification engine on this modeling for the deadlock checks. With various novel ideas to enable the symbolic simulation, bounded model checking (BMC) and invariant checking techniques to work on high-level, our experimental results demonstrate the robustness and effectiveness of the formal deadlock checking on high-level SystemC designs.