Date of Award

3-1991

Document Type

Thesis

Degree Name

Master of Science in Computer Engineering

Department

Department of Electrical and Computer Engineering

Abstract

With the expanding number of components provided on a single digital chip, verification of digital designs is becoming a major problem. The more circuits one places on a single chip, the greater the number of input/output combinations which need to be checked. A paper by Barrow in 1984 discusses a Prolog-based hierarchical formal verification system which he calls VERIFY. Barrow provided a lot of information on what VERIFY can and cannot do, and on projected enhancements. He does not, however, mention how VERIFY actually performs the task of formal verification. This thesis will provide a description of one possible implementation of the formal verification methodology described in VERIFY.

AFIT Designator

AFIT-GCE-ENG-91M-05

DTIC Accession Number

ADA238683

Share

COinS