Equivalence Checking for Function Pipelining in
K. Hao, F. Xie, and S. Ray
In Design, Automation & Test
in Europe (DATE 2010), Dresden, Germany, March 2014. IEEE.
© 2014 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.
Function pipelining is a key transformation in behavioral
synthesis. However, synthesizing the complex pipeline logic
is an error-prone process. Sequential equivalence checking
(SEC) support is highly desired to provide confidence in the
correctness of synthesized pipelines. However, SEC for
function pipelining is challenging due to the significant
difference between the behavioral specification and
synthesized RTL. Furthermore, function pipelines include
hardware logic for dynamically inserting ``bubbles''
(pipeline stalls), which bring additional difficulties in
equivalence checking. We develop an SEC framework for
behaviorally synthesized function pipelines by (1) building
a reference pipeline model with a certified function
pipelining transformation, which faithfully captures bubble
insertion; and (2) checking the equivalence between the
reference model and synthesized RTL. We demonstrate the
scalability of our approach on industry-strength designs
synthesized by a commercial tool.