Applications of symbolic simulation to the formal verification of microprocessors

Functional validation is a major problem in the design of complex hardware systems. This is especially true in microprocessor design, where validation consumes a continually increasing percentage of design resources. Formal verification is often proposed as a solution to this problem, but current techniques have had only limited impact because of scaling problems; the complexity of designs is increasing faster than the capacity of formal verification techniques.; This dissertation presents new ideas that help close the gap between design complexity and formal verification capacity. Two ideas in symbolic simulation greatly expand the applicability of formal verification to commercial design, even in the short term. These ideas have been successfully applied during the design process to find bugs in large submodules of Intel microprocessors. In the longer term, greater strides can be achieved by moving to design practices that embrace higher-level behavioral descriptions. This work develops a technique for verifying out-of-order execution on such descriptions.; Part I describes self consistency, an approach to specification that allows formal verification to be performed without manually creating a formal specification. A reference specification is derived by symbolically simulating the circuit operating with altered inputs or in a different mode. We describe the results of using reference specifications in the verification of two circuits from Intel microprocessor designs.; Part II describes the use of parametric representations of Boolean predicates to control state explosion in BDD-based symbolic simulation. A parametric representation encodes a Boolean predicate as a functional vector. This is useful for constraining verification to a care set and decomposing the care set by data-space partitioning. This technique is much simpler than the more standard structural decomposition approach. Verification results are illustrated for two additional circuits from Intel microprocessor designs.; Part III describes incremental flushing, a technique for verifying out-of-order execution. Out-of-order execution is a difficult verification problem because of the large effective pipeline depth. Incremental flushing is applied to the verification of an out-of-order execution core. An extension to incremental flushing is developed that reduces the amount of manual abstraction required for verification.