Date of Award

12-1991

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Frank M. Brown, PhD

Abstract

The most widely used technique for checking the correctness of digital circuits designs is simulation. As the complexity of digital circuits has continued to grow, however, circuit designers have become unable to perform complete simulations of their integrated circuits. Formal hardware verification provides an alternative approach, performing a series of mathematical proofs in order to show that the construction of the circuit from its submodules will result in the intended overall circuit behavior. Papers by Barrow in 1983 and 1984 discuss a PROLOG-based hierarchical formal circuit verification system named VERIFY. AFIT VERIFY, a simple, experimental reverse-engineered version of Barrow's VERIFY system, was produced by Captain Kevin Sparks in 1991. Since that time, a new user interface has been added to the AFIT VERIFY system, as well as the capability to maintain a central repository of standard, previously verified parts. This thesis provides a detailed description of these and other improvements that have been made to Sparks's AFIT VERIFY system.

AFIT Designator

AFIT-GCE-ENG-91D-06

DTIC Accession Number

ADA243834

Comments

The author's Vita page is omitted.

Download

Share

COinS