中文摘要：

SOC系统级功能验证已成为SOC系统设计周期的瓶颈。本项目确立按统一验证视图和验证信息共享思路建立有效融合各种验证方法和技术的理论框架，在理论和实践上对SOC系统级功能验证取得突破。本项目将设计统一的SOC系统级描述语言；提出SOC系统级测试程序自动生成算法；研究SOC系统级功能覆盖率自动分析技术；研究形式化验证技术对SOC系统级测试程序自动生成和功能覆盖率分析的指导技术。研究基于高层测试生成技术的断言限界模型检验技术；研究模型检验算法优化技术；研究利用模拟信息加速形式化验证的方法和技术。建立SOC系统中IP核之间、软硬件接口和协议的统一形式化模型；研究接口和协议的形式化验证技术。并建立SOC系统级功能验证原型系统。本项目提出和建立的SOC系统级功能验证理论框架和关键技术，能解决现有SOC系统级复合功能验证的主要问题，有效突破SOC系统级功能验证的瓶颈。

结论摘要：

本项目在研究过程中，主要针对SoC系统级建模与描述方法、SoC系统级模拟验证关键技术、SoC系统级形式验证关键技术，以及SoC系统级功能验证原型系统等方面开展研究。研究进展包括对典型的SoC系统，本项目采用基于扩展的实时UML对其进行建模。基于得到各种SoC系统验证模型和SoC系统功能规约, 提出了RTL级基于路径覆盖的模拟矢量自动生成方法、微处理器体系结构级测试程序自动生成方法、SoC系统事务级测试程序自动生成、SoC系统级模拟等方法和技术。提出了RTL级谓词抽象技术、SoC系统级行为抽取与风险评估技术、SoC系统功能行为一致性检查技术、行为级与RTL级等价性检查技术。基于上述研究内容和取得的成果，构建了SoC功能验证原型工具SoC-CBVE、覆盖率驱动的RTL级验证环境HRV、嵌入式微处理器体系结构级验证环境MA2TG，以及基于扩展时间Petri网模型的建模与模拟原型工具PTSE。项目取得一系列成果，在国内外期刊和会议上发表论文17篇。项目构建的原型系统在实际应用中取得了良好效果。