由于片上系统(SoC)的规模和功能在不断膨胀,为了保证设计的正确性,缩短设计的周期,在设计过程中的验证就变得越来越重要,也更为复杂,向业界提出了挑战。　　SoC的验证包括模拟、仿真和形式化验证。本文主要针对基于IP复用的SoC的形式化验证技术进行研究,所取得的主要成果有:　　(1)针对SoC中的AMBA AHB总线协议,提出了一种可以借鉴的形式化建模与验证方法。对AHB总线协议进行了形式化规格;建立了与其规格对应的有限自动机模型;建立协议的SMV模型,以及应用CTL对属性进行了形式描述,借助符号模型检验器SMV对总线无饥饿属性进行验证。　　(2)在分析现有Petri网技术的基础上,提出一种适于嵌入式系统建模的扩展流关系Petri网(EFPN),并对其结构和动态行为规则进行了定义。采用EFPN对乘法器进行了建模,并与另外几种对应的Petri网模型进行了比较;以移动电话系统为例,将EFPN有效地应用于胶合逻辑的建模。　　(3)针对已经建立的EFPN模型,给出一种将EFPN模型转换成对应的时间自动机模型的算法,从而借助模型检验工具UPPAAL完成系统的验证;具体实例的验证结果表明了所提转换算法的可行性。