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) descrip-tion to an RTL implementation. Equivalence checking is critical to ensure that the synthesized RTL conforms to its ESL specification. Such equivalence checking must effec-tively 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 synthe-sized from practical ESL designs. Furthermore, our evalua-tion found a bug in a commercial tool, underlining both the importance of SEC and the effectiveness of our approach