Modular equivalence verification of polynomial datapaths with multiple word-length operands
Bijan Alizadeh, Masahiro Fujita · 2011
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 Z2n1×Z2n2...×Z2ndto Z2n. 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.