Efficient verification with BDDs using implicitly conjoined invariants

Abstract

Many researchers have reported that using 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 are needed to realize the potential advantages of BDD-based verification at the protocol level. Here, we isolate several common causes of BDD-size blowup and show how these problems can be alleviated by a new verification approach based on partially evaluating the invariant being checked into an implicit conjunction of small BDDs. We describe the new method and give several examples of its application.