Representation and Manipulation of Inductive Boolean Functions

Abstract

TV high level of complexity of current hardware systems has led to an interest in formal methods for proving their correctness. Reasoning by induction is a powerful formal proof method with the advantages the a single proof establishes the correctness of an entire family of circuits varying according to some size parameter, and the size of this proof is independent of the size of the circuit. Tautology-checking of symbolic Boolean functions is another method that has been successfully used in formal verification, both for checking equivalence/satisfaction with respect to a functional specification and as a basis for modelchocking. In this paper we present a representation and algorithms for symbolic manipulation of inductive Boolean functions, based on extensions of Binary Decision Diagrams. Our approach allows us to combine reasoning by induction with efficient tautology-checking in an automatic way.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1992
Accession Number
ADA256078

Entities

People

  • Aarti Gupta
  • Allan L. Fisher

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Automatic
  • Computations
  • Computer Science
  • Construction
  • Infinite Series
  • Language
  • Maintenance
  • Observation
  • Reasoning
  • Semantics
  • Simulations
  • Specifications
  • Standards
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.