Efficient translation validation of high-level synthesis

The growing design-productivity gap has made designers shift toward using high-level synthesis (HLS) techniques to generate register transfer level design from high-level languages like C/C++. Unfortunately, this translation process is very complex and is prone to introduce bug into the generated design, which can create a mismatch between what a designer intends and what is actually implemented in the circuit. In this paper, we present an efficient approach to validate the result of HLS against the initial high-level program using translation validation techniques. We redefined the bisimulation relation and proposed a novel algorithm based on it. When compared with the existing method, the proposed method can dramatically reduce the number of automated theorem prover (ATP) querying, which will in turn improve the time cost in equivalence validation. Our method is suitable for structure-preserving transformations such as carried out by Spark synthesizer. We have implemented our validating technique and compared it with a state-of-the-art translation validation method of HLS. The promising results show the effectiveness and efficiency of our method.