Verification algorithms for VLSI synthesis

A description is given of a theory for, and the application of, a general algorithm for determining whether a given multilevel Boolean function is a tautology or whether two given multilevel Boolean functions are equivalent. Four specific cases of this general algorithm are examined. These are termed the flattening method, the don´t-care method, the simulation method, and the algebraic string comparison method. A single unifying algorithm frame is given for the implementation of any of these four methods, depending on parameterization. Experimental results are given which indicate that, with the exception of the don´t-care method, each of these methods has a problem class in which it is clearly superior to the others. The primary application of these algorithms is as a verification tool for silicon compilation systems. However, these algorithms are also being used as the foundation for multilevel logic minimization and automatic test pattern generation programs