Validating Scheduling Transformation for Behavioral Synthesis

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

In Design, Automation & Test in Europe (DATE 2016), Dresden, Germany, March 2016, pages 1652-1657. IEEE.

© 2016 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 automatically compiles an electronic system-level description of a hardware design into an RTL implementation. Scheduling in behavioral synthesis is an important, sophisticated, and error-prone transformation which converts the untimed or partially timed description into a fully timed implementation. We present a scalable equivalence checking algorithm for validating scheduling transformations. Our approach accounts for control/data dependency, scheduling modes, and subtle interface protocols. We successfully validated designs with tens of thousands of lines of RTL synthesized by commercial synthesis tool, demonstrating the viability of our approach.

Relevant files