Implicit and incremental computation of primes and essential primes of Boolean functions

Recently introduced implicit set manipulation techniques have made it possible to formally verify finite state machines with state graphs too large to be built. This paper shows that these techniques can also be used with success to compute and manipulate implicitly extremely large sets of prime and of essential prime implicants of incompletely specified Boolean functions. These sets are denoted by meta-products that are represented with binary decision diagrams. This paper describes two procedures. One is based on the standard BDD operators, and the other, more efficient, takes advantage of the structural properties of BDDs and of meta-products to handle a larger class of functions than the former one. 1 Introduction We have recently introduced a technique [ 4 ] for verifying finite state machines that can deal with machines with state graphs too large to be built. The key concepts that make this verification possible are to denote subsets of f0; 1g @ with their characteristic fu...