| Abstract | SystemC is an efficient system-level modeling language and simulation platform proposed to increase the abstraction level of embedded systems design. However, as the design of systems turns more complex, the exploration of design on a high abstraction level becomes more important than ever. In particular, an important issue to ensure the correction of systems designed with SystemC is how to integrate verification techniques, such as Model-Checking, with the SystemC environment. This paper gives a comparison between of the techniques that can be used to verify SystemC models. A traffic light system is taken as a reference case study and used to demonstrate our practical application. Then, to compares and classifies the existing methodologies according to their capabilities and integral with the SystemC environment. |