  In this paper, we present an efficient formal approach to check the
equivalence of synthesized RTL against the high-level specification in the
presence of pipelining transformations. To increase the scalability of our
proposed method, we dynamically divide the designs into several smaller parts
called segments by introducing cut-points. Then we employ Modular Horner
Expansion Diagram (M-HED) to check whether the specification and implementation
are equivalent or not. In an iterative manner, the equivalence checking for
each segment is performed. At each step, the equivalent nodes and those nodes
which have an impact on them are removed until the whole design is covered. Our
proposed method enables us to deal with the equivalence checking problem for
behaviorally synthesized designs even in the presence of pipelines for nested
loops. The empirical results demonstrate the efficiency and scalability of our
proposed method in terms of run-time and memory usage for several large designs
synthesized by a commercial behavioral synthesis tool. Average improvements in
terms of the memory usage and run time in comparison with SMT- and SAT-based
equivalence checking are 16.7x and 111.9x, respectively.
