Using BDDs to verify multipliers

Bryant’s Binary Decision Diagrams (BDDs) [6] have been successfully used for verifying combinational circuits [12, 181. However, multiplier circuits are difficult to verify using BDDs since the size of the BDD representing multiplication grows exponentially in the number of input bits [6, 71. This paper presents a method for using BDDs to verify multipliers that avoids this exponential complexity. The method has been used to verify a 16 by 16 bit combinational multiplier, the C6288 circuit from the ISCAS85 benchmarks [5]. This is the only ISCAS85 benchmark circuit that could not be verified using the techniques described by Fujita et al. [12] and Malik et al. [la].