A Survey of Verification for High-level Synthesis

被引：0
作者：
Hu J. [1 ]
Hu Y. [1 ]
Wang G. [1 ]
Chen G. [1 ]
Yang H. [1 ]
Kang Y. [1 ]
Wang K. [1 ]
Li S. [2 ]
机构：
[1] Sixty-third Institute, National University of Defense Technology, Nanjing
[2] School of Computer, National University of Defense Technology, Changsha
来源：
| 1600年 / Institute of Computing Technology卷 / 33期
关键词：
Bisimulation; Finite state machine with datapath; Formal me-thod; High-level synthesis; Path verification;
D O I：
10.3724/SP.J.1089.2021.18394
中图分类号：
学科分类号：
摘要：
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. © 2021, Beijing China Science Journal Publishing Co. Ltd. All right reserved.
引用
收藏
页码：287 / 297
页数：10
相关论文
共 73 条
[1]  
Gupta S, Gupta R K, Dutt N D, Et al., Spark: a parallelizing approach to the high-level synthesis of digital circuits, (2004)
[2]  
de Micheli G., Synthesis and optimization of digital circuits, (1994)
[3]  
Zhang Z R, Fan Y P, Jiang W, Et al., AutoPilot: a platform-based ESL synthesis system, pp. 99-112, (2008)
[4]  
Koch D, Hannig F, Ziener D., FPGAs for software programmers, (2016)
[5]  
Aho A V, Sethi R, Ullman J D., Compilers, principles, techniques and tools, (1986)
[6]  
Yang Z K, Hao K C, Cong K, Et al., Equivalence checking for compiler transformations in behavioral synthesis, Proceedings of the 31st International Conference on Computer Design, pp. 491-494, (2013)
[7]  
Yang Z K, Hao K C, Cong K, Et al., Scalable certification framework for behavioral synthesis front-end, Proceedings of the 51st ACM/EDAC/IEEE Design Automation Conference, pp. 1-6, (2014)
[8]  
Shankar S, Fujita M., Rule-based approaches for equivalence checking of SpecC programs, Proceedings of the 6th International Conference on Formal Methods and Models for Co-Design, pp. 39-48, (2008)
[9]  
Yoshida H, Fujita M., Improving the accuracy of rule-based equivalence checking of system-level design descriptions by identifying potential internal equivalences, Proceedings of the 10th International Symposium on Quality of Electronic Design, pp. 366-370, (2009)
[10]  
Hu J, Wang G W, Chen G L, Et al., Equivalence checking between system-level descriptions by identifying potential cut-points, Proceedings of International Conferences on Communications, Signal Processing, and Systems, pp. 1328-1335, (2019)
12345678