Validating Scheduling Transformation for Behavioral Synthesis
Automation & Test in Europe (DATE 2016), Dresden,
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.