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