|
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.
| |