Formal Co-verification for SoC design with colored Petri net

Abstract

The complexity of SoC is increasing rapidly. It is an important trend that SoC design is always based on the reuse of both IP cores and software components. In consequence, new verification techniques are needed, which overcome the limitations of traditional methods and are suitable for SoC at the same time. This paper introduces a computational model for SoC based on colored Petri net, formulates the IP cores, components and user defined logics, and presents a method to translate the architecture design into the colored Petri net model. And a formal co-verification approach of SoC using CPN tools is also proposed. The method concentrates on verifying the correctness of the design. An example of the audio and video architecture design of the PDA platform illustrates the effectiveness of our approach on practical applications. Finally, the experimental results are given. © Springer-Verlag Berlin Heidelberg 2005.