CAJ | 학술논문

给传统嵌入式系统验证方法带来巨大挑战的是SoC设计中硬件部分采用IP核、软件部分采用构件技术,这就需要一种既能克服传统方法缺陷又能适合SoC的新方法.针对SoC提出了一种基于着色Petri网的数学模型,形式化定义了IP核、构件和用户自定义逻辑模块,并阐述了从SoC设计体系结构到着色Petri网模型的转换方法,还介绍了如何利用现有工具CPN Tools来分析Petri网模型.该方法不仅能验证SoC设计的正确性,还能验证其时间性,一旦给出SoC设计中IP核、构件和用户自定义逻辑的体系结构,那么就能够验证出整个系统的设计正确性和时间性,最后通过一个验证PDA手机音频和视频子系统的例子证明该方法行之有效,并给出了相应的实验结果.
급전통감입식계통험증방법대래거대도전적시SoC설계중경건부분채용IP핵、연건부분채용구건기술,저취수요일충기능극복전통방법결함우능괄합SoC적신방법.침대SoC제출료일충기우착색Petri망적수학모형,형식화정의료IP핵、구건화용호자정의라집모괴,병천술료종SoC설계체계결구도착색Petri망모형적전환방법,환개소료여하이용현유공구CPN Tools래분석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.