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 条
[21]  
Dovier A, Piazza C, Policriti A., An efficient algorithm for computing bisimulation equivalence, Theoretical Computer Science, 311, 1-3, pp. 221-256, (2004)
[22]  
Baier C., Polynomial time algorithms for testing probabilistic bisimulation and simulation, Proceedings of International Conference on Computer Aided Verification, pp. 50-61, (1996)
[23]  
Baier C, Engelen B, Majster-Cederbaum M., Deciding bisimilarity and similarity for probabilistic processes, Journal of Computer and System Sciences, 60, 1, pp. 187-231, (2000)
[24]  
Eveking H, Hinrichsen H, Ritter G., Automatic verification of scheduling results in high-level synthesis, Proceedings of International Conference on Design, Automation and Test in Europe, pp. 260-265, (1999)
[25]  
Necula G C., Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 83-94, (2000)
[26]  
Kundu S, Lerner S, Gupta R., Validating high-level synthesis, Proceedings of the 20th International Conference on Computer Aided Verification, pp. 459-472, (2008)
[27]  
Bandyopadhyay S, Sarkar D, Banerjee K, Et al., A path-based equivalence checking method for petri net based models of pro-grams, Proceedings of the 10th International Joint Conference on Software Technologies, pp. 319-329, (2015)
[28]  
Bandyopadhyay S, Sarkar D, Mandal C., Poster: an efficient equivalence checking method for petri net based models of pro-grams, Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, pp. 827-828, (2015)
[29]  
Cortes L A, Eles P, Peng Z B., Verification of embedded systems using a petri net-based representation, Proceedings of the 13th International Symposium on System Synthesis, pp. 149-155, (2000)
[30]  
Bandyopadhyay S, Sarkar S, Sarkar D, Et al., SamaTulyata: an efficient path based equivalence checking tool, Proceedings of International Symposium on Automated Technology for Verification and Analysis, pp. 109-116, (2017)
12345678