Scalable Certification Framework for Behavioral Synthesis Front-End

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

In S. Hassoun, C. Alpert, and S. Hu editors, 51st International ACM/EDAC/IEEE Design Automation Conference (DAC 2014), San Francisco, CA, USA, June 2014. ACM.

© 2014 ACM, 2 Penn Plaza, Suite 701 New York, New York 10121. Permission to make digital or hard copies of portions of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page in print or the first screen in digital media. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Send written requests for republication to ACM Publications, Copyright & Permissions at the address above or fax +1 (212) 869-0481 or email For other copying of articles that carry a code at the bottom of the first or last page, copying is permitted provided that the per-copy fee indicated in the code is paid through the Copyright Clearance Center, 222 Rosewood Drive, Danvers, MA 01923.


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. In this paper, we present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis front-end. Our approach makes use of dual-rail symbolic simulation of the input and output of a transformation, together with identification and inductive verification of their loop structures. We have evaluated our framework on transformations applied by an open source behavioral synthesis tool to designs from the CHStone benchmark. Our tool can automatically validate more than 75 percent of the total of 1008 compiler transformations applied, taking an average time of 1.5 seconds per transformation.

Relevant files