Optimizing Equivalence Checking for Behavioral Synthesis
K. Hao, F. Xie, S. Ray, and J. Yang
In Design, Automation & Test
in Europe (DATE 2010), Dresden, Germany, March 2010. IEEE.
© 2009 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 is the compilation of an Electronic system-level
(ESL) design into an RTL implementation. We present a suite of
optimizations for equivalence checking of RTL generated through
behavioral synthesis. The optimizations exploit the high-level
structure of the ESL description to ameliorate verification
complexity. Experiments on representative benchmarks indicate that
the optimizations can handle equivalence checking of synthesized
designs with tens of thousands of lines of RTL.