片上系统高层等价性检验理论与关键技术

System level verification has become the bottleneck of the SoC system design process. To solve the problems such as duplicated work and low verification efficiency in system level designs brought by huge differences among them, this proposal focuses on theory and technology of equivalence checking between SoC system level designs and try to make break through. The research topics include equivalence checking of optimizting transformation for behavioral synthesis, equivalence checking of scheduling transformation for behavioral synthesis, equivalence checking of manual transformation. We are going to break through in following key areas such as model abstraction and simplification, timing matching, mapping information extraction, cut-point identification, path verification and extension. Finally, we will establish theory framework for SoC system level equivalence checking and implement prototype of a series of tools to support SoC high-level equivalence checking. The research results are of great significance to promote design of self-copyright SoC chips and to improve the level and scale of integrated circuit design in China.

系统级功能验证已经成为片上系统（System-on-a-Chip,SoC）设计进程的瓶颈。针对SoC系统级功能验证各层巨大差异带来的重复工作多、验证效率低下等突出问题，本项目研究SoC高层等价性检验技术，在理论和实践上对SoC系统级功能验证取得突破。研究SoC高级综合前端优化前后等价性检验、SoC高级综合后端调度前后等价性检验和人工转换过程的等价性检验技术，突破高层等价性检验遇到的高层模型抽象与化简、时序匹配、映射关系提取、割点识别和路径扩展与验证等关键科学问题，建立SoC高层等价性检验理论，实现支持SoC高层等价性检验的系列工具原型。它的研究成果，对促进我国研究设计自主版权的SoC芯片，提高集成电路设计水平和规模有重大意义。

本项目研究了SoC高层等价性检验技术，在理论和实践上对SoC系统级功能验证取得了突破。研究了SoC高级综合前后和人工转换过程的等价性检验算法，研究了高层模型抽象与化简、时序匹配、映射关系提取、割点识别和路径扩展与验证等关键科学问题，建立了SoC高层等价性检验理论，实现了支持SoC高层等价性检验的系列工具原型。..在系统级与RTL级等价性检验算法上：（1）提出了利用潜在等价点进行设计划分的等价性检验算法，利用模拟产生的潜在等价点将待验证设计进行划分，逐步验证整个设计，实验表明算法能够处理更大规模的设计。（2）提出了多线程并行模拟验证算法，利用多线程技术同时模拟待验证设计，比较模拟结果，从而得到设计的等价性，极大提高了传统模拟方法的验证效率。在高级综合过程中的等价性检验算法上：（1）通过定义活跃变量和提高等价路径判定条件，提出了解决GCSE调度的等价性检验算法，实验表明我们提出的算法能有效解决非公共变量引起的GCSE不等价问题。（2）针对VP算法在循环调度中存在的错误否定问题，提出了基于深度路径的改进VP算法，算法能够排除现有VP算法中不会执行的路径，解决了目前VP算法中存在的错误否定问题。..通过基金委对本项目的资助，项目负责人得以迅速成长（晋升副教授），形成了具有自身特色的研究队伍，在一定程度上解决了片上系统高层等价性检验的相关问题，完成了预期的目标。在本项目资助下，课题组以第一作者或通讯作者发表论文9篇，其中CCF推荐A/B/C论文3篇，SCI或EI检索论文9篇；开发出4个等价性检验相关原型工具；培养硕士毕业生2人。