Formal Deadlock Checking on High-Level SystemC Designs
Journal
IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
Pages
794-799
Date Issued
2010-11
Author(s)
Abstract
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 highlevel 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. ©2010 IEEE.
Type
conference paper