Equivalence checking of scheduling in high-level synthesis

By adopting high level synthesis tools, electronic system level designs provide a promising solution to fill the growing design-productivity gap of high-quality hardware system. Unfortunately, the synthesis process is very complex and error prone. In this paper, we present a novel approach on equivalence checking of scheduling in high-level synthesis. Our approach combines the translation validation, cut-point and shared-value graphs techniques, and provides a unified framework to deal with various scheduling optimizations efficiently. We have implemented our approach and some empirical experimental results are provided. The promising results show the effectiveness and efficiency of the proposed method.