Equivalence Checking for Compiler Transformations in Behavioral Synthesis

Z. Yang, K. Hao, K. Cong, S. Ray, and F. Xie

In G. Byrd, K. Schneider, N. Chang, and S. Ozev editors, Proceedings of the 31st IEEE International Conference on Computer Design (ICCD 2013), Asheville, NC, USA, October 2013, pages 491-494. IEEE.

© 2013 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


Behavioral 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. We present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis. Our approach is based on dual-rail symbolic simulation of the input and output design representations of a transformation. We have evaluated our framework on transformations applied to several designs by an open source behavioral synthesis tool, and we present initial results demonstrating the approach.

Relevant files