A Static Analysis Approach for Verification of Synchronization Correctness of SystemC Designs

In this paper a novel approach for verification of synchronization correctness of HLS-synthesizable SystemC designs is proposed. Synchronization correctness is formulated in terms of statement reach ability properties which makes it applicable to clocked, asynchronous and mixed designs. It allows automatic detection of deadlocks and concurrent data modification. Live lock detection and invariant checking are supported through user assertions. Our approach is based on static analysis methods. We have implemented our approach in Aegis tool that supports a large subset of C++, SystemC and STL. We applied it on multiple designs with more than 30 KLOC of unique code in total, including a number of industrial designs, and detected some real synchronization errors. Our experiments show that analysis complexity grows linearly with the number of analyzed clock ticks and estimated precision is about 80%.