Formal Verification of GCSE in the Scheduling of High-level Synthesis: Work-in-Progress

High-level synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a register-transfer level (RTL) implementation. However, an error may exist in the RTL implementation from the compiler in the high-level synthesis due to the complex and error prone compiling process. Global common subexpression elimination (GCSE) is a commonly used code motion technique in the scheduling of high-level synthesis. In this paper, we present an equivalence checking method to verify GCSE in the scheduling of high-level synthesis by enhancing the path equivalence criteria. The initial experimental results demonstrate our method can indeed verify the GCSE which has not been properly addressed in the past.