Accession Number : ADA292236

Title :   Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction.

Descriptive Note : Doctoral thesis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Gupta, Aarti

PDF Url : ADA292236

Report Date : 31 OCT 1994

Pagination or Media Count : 227

Abstract : The high level of complexity of current hardware systems has led to an interest in formal methods for proving their correctness. This thesis presents a methodology for formal verification of inductively-defined hardware, based on automatic symbolic manipulation of classes of inductive Boolean functions (IBFs). It combines reasoning by induction and symbolic tautology-checking in a way that incorporates the advantages of both, where the key idea is that by building an inductive argument into the IBF representations, explicit proofs by induction can be avoided. The methodology consists of identifying classes of inductive Boolean functions that are useful for representation of hardware and specifications, associating a schema with each class (consisting of a canonical representation and symbolic manipulation algorithms), and appropriately manipulating these representations for performing formal verification.

Descriptors :   *VERIFICATION, *COMPUTERS, METHODOLOGY, COMPUTER AIDED DESIGN, REASONING, THESES, PROBLEM SOLVING, CIRCUITS, AUTOMATIC, INDUCTION SYSTEMS.

Subject Categories : Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE