The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.11 - November (1997 vol.46)
pp: 1230-1245
ABSTRACT
<p><b>Abstract</b>—A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), is proposed to provide a compact representation for functions whose Ordered Binary Decision Diagram (OBDD) representation is intractably large. We explain properties of IBDDs and present algorithms for constructing IBDDs from a given circuit. Practical and effective algorithms for satisfiability testing and equivalence checking of IBDDs, as well as their implementation results, are also presented. The results show that many functions, such as multipliers and the hidden-weighted-bit function, whose analysis is intractable using OBDDs, can be efficiently accomplished using IBDDs. We report efficient verification of Booth multipliers, as well as a practical strategy for polynomial time verification of some classes of unsigned array multipliers.</p>
INDEX TERMS
Boolean functions, BDDs, canonical representations, free BDDs, graph representations, IBDDs, OBDDs, satisfiability, verification.
CITATION
James Bitner, Magdy S. Abadir, Jawahar Jain, Donald S. Fussell, "Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions", IEEE Transactions on Computers, vol.46, no. 11, pp. 1230-1245, November 1997, doi:10.1109/12.644298
21 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool