A methodology for verification of embedded systems based on systemc

In the design of complex systems that use an intellectual property components (IP), a functional and compositional verification are an important part in the design process. A verification process of reusable IP blocks is usually performed by using formal methods since the second technique that is the simulation has several shortcomings. IP blocks are often described by hardware description languages such as VHDL and SystemC. In this paper, we present a methodology which we automatically generate formal synchronous models from existing non-formal system level design descriptions that integrates smoothly into existing co-design flows. This generation pass is performed in tow steps: structural extraction and behavioral extraction. We exemplify the methodology with the popular system design SystemC language and the flexible and expressive synchronous dataflow formalism of SIGNAL.