Reducing BDD size by exploiting functional dependencies

Abstract

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.