针对SoC设计正确性和时间性的形式化协同验证方法(英文)

Formal Co-verification for the Correctness and Timing Requirements of SoC Design

给传统嵌入式系统验证方法带来巨大挑战的是SoC设计中硬件部分采用IP核、软件部分采用构件技术,这就需要一种既能克服传统方法缺陷又能适合SoC的新方法。针对SoC提出了一种基于着色Petri网的数学模型,形式化定义了IP核、构件和用户自定义逻辑模块,并阐述了从SoC设计体系结构到着色Petri网模型的转换方法,还介绍了如何利用现有工具CPNTools来分析Petri网模型。该方法不仅能验证SoC设计的正确性,还能验证其时间性,一旦给出SoC设计中IP核、构件和用户自定义逻辑的体系结构,那么就能够验证出整个系统的设计正确性和时间性,最后通过一个验证PDA手机音频和视频子系统的例子证明该方法行之有效,并给出了相应的实验结果。

SoC design is always based on the reuse of both IP cores in hardware and components in software, which challenges the traditional verification of embedded systems. 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 of SoC into the colored Petri net model. A formal co-verification approach of SoC using CPN tools is also proposed. The method can verify not only the design correctness but also the timing requirements of SoC. Once the architecture design of the IP cores, components and user defined logics are defined, the correctness and timing requirements of the whole system can be verified. Finally, an example of the audio and video architecture design of the PDA platform illustrates the effectiveness of our approach on practical applications. And the experimental results are given.