Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 31, 1994
- Accession Number
- ADA292236
Entities
People
- Aarti Gupta
Organizations
- Carnegie Mellon University