Accession Number : ADA136466

Title :   Verification of Hardware Design Correctness: Symbolic Execution Techniques and Criteria for Consistency.

Descriptive Note : Techncial rept.,


Personal Author(s) : Cory,W E

PDF Url : ADA136466

Report Date : Jun 1983

Pagination or Media Count : 118

Abstract : 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.

Descriptors :   *Digital computers, *Systems engineering, *Computer program verification, Computer architecture, Methodology, Consistency, Computerized simulation, Corrections, Test and evaluation

Subject Categories : Administration and Management
      Computer Programming and Software
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE