A Survey of Verification for High-level Synthesis

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.