Reducing BDD Size by Exploiting Functional Dependencies

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 believe that new techniques will be needed to realize the potential advantages of BDD verification at the protocol level. Here, we identify functionally 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 exponentially-sized problem to a provably O(n log n)-sized one, achieving several orders of magnitude reduction in BDD size.