Reducing BDD size by exploiting functional dependencies
Alan J. Hu, David L. Dill · 1993
Many researchers have reported that the use of Boolean decision diagrams (BDDs) greatly increases the size of hardware designs that can be formally verified automatically.Our own experience with automatic verification of high-level aspects of hardware design, such as protocols for cache coherence and communications, contradicts previous results; in fact BDDs have been substantially inferior to brute-force algorithms that store states explicitly in a table.We betieve that new techniques will be needed to realize the potential advantages of BDD verification at the protocol level.Here, we identify &nctionally dependent variables as a common cause of BDD-size blowup, and describe new techniques to avoid the problem.Using the improved algorithm, we reduce an exponentiallysized problem to a provably O(n log n)-sized one, achieving several orders of magnitude reduction in BDD size.