Optimizing equivalence checking for behavioral synthesis

Abstract—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.

• Type: Conference
• Year: 2010
• Where: DATE
• Authors: Kecheng Hao, Fei Xie, Sandip Ray, Jin Yang
• Keywords: Abstract—Behavioral Synthesis, DATE 2010, Equivalence Checking, Hardware, RTL Implementation