Verification of Data-path and Controller Generation Phase of High-level Synthesis
C Karfa, D Sarkar, C Mandal
Abstract
     

The paper describes a verification method of data-path and controller generation phase of high-level synthesis (HLS) process. The goal is achieved in two steps. In step 1, the generated RTL description is analyzed to obtain the register transfer (RT) operations executed in the data-path for a given control assertion pattern in each control step and in step 2, an equivalence checking method is proposed to verify the correctness of the controller. The method is im- plemented and integrated with an existing HLS tool, called SAST. The experimental results on several HLS benchmarks prove the effectiveness of the proposed method.

     
     
     
Keywords: FSMD model, equivalence checking, formal verification, high-level synthesis


     
chitta@iitkgp.ac.in [Full paper and publications list]