Handling design and implementation optimizations in equivalence checking for behavioral synthesis

Behavioral synthesis involves generating hardware design via compilation of its Electronic System Level (ESL) description to an RTL implementation. Equivalence checking is critical to ensure that the synthesized RTL conforms to its ESL specification. Such equivalence checking must effectively handle design and implementation optimizations. We identify two key optimizations that complicate equivalence checking for behavioral synthesis: (1) operation gating, and (2) global variables. We develop a sequential equivalence checking (SEC) framework to compare ESL designs with RTL in the presence of these optimizations. Our approach can handle designs with more than 32K LoC RTL synthesized from practical ESL designs. Furthermore, our evaluation found a bug in a commercial tool, underlining both the importance of SEC and the effectiveness of our approach.