Automatic structural abstraction techniques for enhanced verification

Abstract

Computers have become central components of nearly every facet of modern life. Advances in hardware development have resulted in computers more powerful than the largest mainframe of the last decade becoming available and affordable for general use. This in turn has enabled problems which were historically intractable to become solvable with present technologies. This trend has been noted for four decades. Functional verification is the process of validating that a design conforms to its specification. Exhaustive verification generally requires exponential resources with respect to design size, hence there is a fine line between “solvable” and “intractable”; this cut-off point is unfortunately often far smaller than that which is practically necessary. Due to ongoing increases in hardware design size, direct application of exhaustive techniques to verify these designs requires exponentially-growing verification resources which outpaces available boosts in computing power. Therefore, on the surface, Moore’s law works against the hardware verification community. This thesis presents an approach to battling verification complexity via automatic abstraction techniques which transform the structure of a design. These techniques require ix only polynomial resources with respect to design size, and may yield exponential speedups to the verification process. These abstractions are developed as components of a modular transformation-based verification framework, enabling optimal synergy between the various techniques. Our specific contributions include: 1) a compositional and structural diameter overapproximation technique, enabling the use of abstractions to tighten the produced bounds; 2) an on-the-fly retiming technique for redundancy removal; 3) the concept of fanin register sharing to enhance min-area retiming; 4) a generalized retiming approach which eliminates reset state and input-output equivalence constraints, and supports negative registers; 5) structural cut-based abstraction; 6) a structural target enlargement approach; 7) the technique of -slow abstraction; and 8) the technique of phase abstraction. Numerous experiments demonstrate the utility and synergy of these techniques in simplifying difficult problems. We therefore feel that these techniques comprise a significant step towards a scalable, automated verification system, helping to realize the prediction made by E. Allen Emerson that “Someday, Moore’s Law will work for us [the verification community], rather than against us.”