Verifying the circuit implementation of Boolean functions against their abstract specifications is a fundamental and difficult problem in circuit design. This paper presents a graph-theoretical representation, the indexed binary decision diagram (IBDD), that facilitates this task. IBDD is a relaxation of the earlier ordered binary decision diagrams (OBDD). The advantage of the new representation over OBDD is its smaller size, which allows for more practical algorithms. In particular, the authors use the IBDD representation for effective verification of Booth multipliers and some classes of unsigned array multipliers. The price for the more compact representation is paid in the verification of the equivalence of IBDDs, because many nonisomorphic diagrams can represent the same Boolean function. Several strategies for verifying equivalence are proposed. Experimental results of IBDD-based methods for Booth multipliers and hidden-weighted bit functions provide insight into time requirements as a function of the number of variables. The observed running times for these functions are polynomial and compare favorably with the exponential growth of verification techniques derived from the OBDD representation.