Automated Formal Equivalence Verification of Pipelined Nested Loops in Datapath Designs

Payman Behnam, Bijan Alizadeh, Sajjad Taheri

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 transformation…