Verification of Hardware Design Correctness

This thesis investigates two aspects of the functional verification problem in digital hardware design. It discusses the reduction of case splitting in the symbolic execution of event-driven simulations and defines criteria for consistency between two hardware descriptions. Symbolic executions of event-driven simulations tend to split into many subcases due to the event detection mechanism. The substitution of non-selective trace for selective trace eliminates this case splitting for combinational elements. In general, an inductive assertion analysis or a symbolic execution test can determine whether the substitution is correct for a particular element. Case merging using conditional expressions is a more general technique for eliminating case splitting but it tends to generate complex symbolic expressions. Case merging is most likely to be beneficial for functional verification when the simulation relation is sparse and the symbolic expression complexity grows slowly. This thesis defines a criterion that applies to both deterministic and nondeterministic models, with and without don't-cares. Hierarchical verification is demonstrated for the new criterion. This criterion is also modified to facilitate the verification of programs with loops. It is shown to retain intuitive notions of correctness captured by the first criterion. Finally, a modification of the hierarchical design methodology allows the application of Brand's theorem for partitioned verification even when the design introduces new timing details. The introduction of new timing details is performed separately from the introduction of new structural detail.