Static analysis method for deadlock detection in SystemC designs

One of the goals of SystemC is high level system design verification at the early stage. Currently, simulation is widely used for this purpose. As the level of design parallelism grows, efficiency of simulation-based verification methods decreases. Thus different formal verification methods for SystemC are actively researched. In this paper we present an approach to deadlock detection in SystemC designs based on static code analysis. Our approach to static analysis considers SystemC scheduler semantics. The developed approach has been implemented in Deadlock Analyzer tool. We demonstrate efficiency of our tool by applying it to dining philosophers, crossroads, producer-consumer cases and to a real-life model of video accelerator.