随着大规模集成电路工艺的不断提高以及嵌入式系统功能需求等多方面要求的日益增加，寻找正确有效地进行嵌入式系统设计的方法成为一种普遍需求，相关的研究也被广泛地展开。 ASIP(ApplicationSpecificInstruction-setProcessors)是针对特定应用领域而设计的，是兼具ASIC(ApplicationSpecificIntegratedCircuits))的高性能和GPP(GeneralPurposeProcessor)的灵活性的一类特殊的处理器，在嵌入式系统中的应用越来越多。我们采用的是基于体系结构描述语言(ADL)驱动的体系结构设计空间搜索DSE的ASIP设计方法，因此，在设计初期保证设计的正确性，以及在整个自上而下的设计流程中保证必要的属性被保留，即保证设计的一致性，可以减少后期改正或重新设计的代价。业界在对设计正确性进行检验时主要是采用仿真的方法，但是由于其固有的局限性，形式化方法被提出，并得到广泛的应用。 本论文在对国内外主要的形式化验证技术进行深入研究的基础上，结合ADL驱动的ASIP设计流程的特点，提出一种基于Petri网的形式化建模和验证技术。主要工作如下： 提出PNP(PetriNetrepresentationforPipelinemodeling)模型，给出其定义和建模方法，以及PNP模型中的层次和等价等概念，用于基于模型的验证。 提出了两种基于PNP模型进行ASIP验证的方法，一是使用已有的模型检验工具，用于系统状态相关的验证；另一个是基于Petri网模型的仿真，用于系统行为相关的验证。 最后，我们将基于PNP模型的建模及验证与我们的设计开发环境相结合，提出了由xpADL体系结构描述自动生成PNP模型的方法，以满足设计流程对形式化建模的要求。 上述研究，对构成完整的ASIP体系结构设计环境有重要的意义。