A Prolog-Based System for Hardware Verification

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1991
Accession Number
ADA238683

Entities

People

  • Kevin L. Sparks

Organizations

  • Air Force Institute of Technology

Tags

Communities of Interest

  • Advanced Electronics
  • Autonomy
  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Circuits
  • Classification
  • Computer Programming
  • Computers
  • Digital Circuits
  • Engineering
  • Language
  • Logic
  • Logic Gates
  • Nand Gates
  • Procedural Programming
  • Programming Languages
  • Prototypes
  • Simulations
  • Standards
  • War Colleges

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Naval Engineering and Maritime Security