片上多核处理器验证理论与关键技术

针对片上多核处理器验证中设计规模大、验证效率低、完备性不足、存储结构与互连网络验证复杂、硅后验证困难等突出问题，研究突破片上多核处理器高层次建模与多视图协同验证方法、面向事务层与系统层的高效形式验证引擎优化方法、基于SMT的片上网络可验证性综合、基于二维抽象的存储一致性协议验证、事务级模型与RTL描述的等价性验证、半形式化的全芯片模拟验证、硅后验证辅助技术等理论与关键技术，建立高层次、可扩展的片上多核处理器高层次验证理论方法体系，实现支持片上多核处理器验证的系列工具原型，有效提高片上多核处理器验证效率、完备性和可信性，并将研究成果直接应用于"银河飞腾"系列多核CPU与DSP的验证实践。.所研究建立的模型、理论框架、方法在验证科学领域达到国际领先水平，为我国自主高性能微处理器的可持续发展奠定坚实基础。

针对片上多核处理器验证中设计规模大、验证效率低、完备性不足、存储结构与互连网络验证复杂、硅后验证困难等突出问题，研究突破片上多核处理器高层次建模与多视图协同验证方法、面向事务层与系统层的高效形式验证引擎优化方法、基于SMT 的片上网络可验证性综合、基于二维抽象的存储一致性协议验证、事务级模型与RTL 描述的等价性验证、半形式化的全芯片模拟验证、硅后验证辅助技术等理论与关键技术，建立可扩展的片上多核处理器高层次验证理论方法体系，实现支持片上多.核处理器验证的系列工具原型，有效提高片上多核处理器验证效率、完备性和可信性。在项目执行期间取得多项创新成果，包括：多核处理器体系结构事务级建模方法和多视图协同验证方法，极小SMT不可满足子式求解算法，对偶综合中自动推导前提断言方法，参数化协议的状态空间化简方法，基于模拟与机器学习的系统级等价性验证方法等。在IEEE TCAD、Journal of Supercomputing、ACM TODAES等国际期刊和本领域重要的国际会议上发表论文55篇，其中SCI期刊发表论文15篇，EI论文34篇。培养研究生44名，申请国家发明专利12项。理论研究成果有力支撑了飞腾系列CPU和DSP微处理器的验证实践。