Abstract
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.
