Accession Number:

ADA243834

Title:

Formal Verification of Digital Logic

Descriptive Note:

Master's thesis

Corporate Author:

AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH SCHOOL OF ENGINEERING

Personal Author(s):

Report Date:

1991-12-01

Pagination or Media Count:

210.0

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 Barrows 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 Sparkss AFIT VERIFY system.

Subject Categories:

  • Electrical and Electronic Equipment
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE