Modular equivalence verification of polynomial datapaths with multiple word-length operands

In this paper, we extend Modular Horner Expansion Diagram (Modular-HED) as a canonical polynomial representation to verify polynomial functions with multiple bit-width operands from Z_2n1×Z_2n2...×Z_2nd to Z_2n. Our contributions are mostly in efficient implementation of [1] with a canonical decision diagram in such a way that both verification and synthesis of large arithmetic circuits can be more efficient. The experimental results show the effectiveness of our approach in comparison with other decision diagrams and algebraic techniques.