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.”
Department
Description
text