SoC高级综合验证研究进展  

A Survey of Verification for High-level Synthesis

作　　者：胡健[1] 胡永扬 王观武[1] 陈桂林 杨海涛[1] 康云 王康 李思昆[2] Hu Jian;Hu Yongyang;Wang Guanwu;Chen Guilin;Yang Haitao;Kang Yun;Wang Kang;Li Sikun(Sixty-third Institute,National University of Defense Technology,Nanjing 210000;School of Computer,National University of Defense Technology,Changsha 410000)

机构地区：[1]国防科学技术大学第六十三研究所,南京210000 [2]国防科学技术大学计算机学院,长沙410000

出　　处：《计算机辅助设计与图形学学报》2021年第2期287-297,共11页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(61902421).

摘　　要：针对近年来片上系统(system on chip,SoC)高级综合验证领域的工作,首先分析了高级综合验证的难点,然后根据应用领域将算法分为3类:高级综合前端验证算法、高级综合调度验证算法和高级综合后端验证算法.同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高级综合验证算法目前面临的映射关系缺失、状态空间爆炸和复杂的数据结构等挑战,并对该领域今后的研究方向进行了展望.For the recent research in the verification of high-level synthesis for SoC,this paper analyzes the difficulties on formal verification for high-level synthesis,and classifies the recent research works to 3 classes according to the algorithm types.The algorithms are classified to high-level synthesis verification algorithms for front-end,high-level synthesis verification algorithms for scheduling and high-level synthesis verification algorithms for back-end.Then,the advantages,disadvantages and the used techniques of the existing algorithms are analyzed.Finally,the existing challenges including lack of mapping information,state explosion and complex data structure and future research directions in formal verification for high-level synthesis are discussed.

关 键 词：高级综合 带数据通路的有限状态机 互模拟关系 路径验证 形式化方法 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]