A STATIC ANALYSIS APPROACH FOR FORMAL VERIFICATION OF SYSTEMC DESIGNS

A novel approach for formal verification of SystemC designs is presented which is based on static analysis and logical inference. It allows to specify and to verify properties of SystemC processes as functions over time. Part of that approach is the new “Aegis FDL ” language for property specification. Furthermore, we wrote a plug-in for the gnu gcc compiler which represents the SystemC design internally by a control flow graph. A subsequent time course analysis is applied to obtain the process ’ states at all simulated points in time. Property checking is implemented by selective linear definite resolution and allows to check assertions and to identify inactive branches. The applicability of the approach is shown by an example