Formal Analysis of Integer Multipliers by building Binary Decision Diagram of Adder Trees

Jitendra Kumar1, Asutosh Srivastava1, Masahiro Fujita2
1Jawaharlal Nehru University, 2University of Tokyo


Reduced Ordered Binary Decision Diagram (ROBDD) traditionally gives a compact and canonical representation of useful logic functions for a given order of variables that have been utilized in logic synthesis and verification. For multiplication functions, however, BDD grows exponentially with the number of inputs. The experimental result shows that BDDs can be built up to 18 − bits integer multipliers, as the number of nodes in BDD becomes too large to manipulate. The previous study shows, instead of building BDDs of a multiplier circuit using original input variables, by using all partial products as variables for BDD, the size of the BDD is limited to 4th- degree polynomial of the number of the inputs. Integer multiplication can be partitioned into two phases: partial product generation and its summation. In this paper, targeting multipliers using simple partial products, we explored and studied a novel approach to construct BDDs mostly for the summation phase. This dramatically reduces the final BDD size and we were able to build BDDs for the primary outputs of the multipliers with the size of 3rd- degree polynomial. Further, we proposed and studied a new algorithm for equivalence checking between two multiplier circuits of different architectures using our BDD construction method. The experimental results show that our proposed method is capable of verifying wide verities of multipliers up to 32 − bits even after optimization.