Efficient algorithmic circuit verification using indexed BDDs

The Indexed Binary Decision Diagram (IBDD), a Boolean function representation scheme, provides a compact representation for functions whose OBDD representation is intractably large. In this paper, we present more efficient algorithms for satisfiability testing and equivalence checking of IBDDs. Efficient verification of Booth multipliers, as well as practical strategies for polynomial time verification of some classes of unsigned array multipliers, are demonstrated experimentally. Our results show that the verification of many instances of functions whose analysis is intractable using OBDDs, such as multipliers and the hidden-weighted-bit function, can be done efficiently using IBDDs.<>