Approximate Reachability With BDDs Using Overlapping Projections

Abstract

Approximate reachability techniques trade off accuracy with the capacity to deal with bigger designs. Cho et al proposed approximate FSM traversal algorithms over a partition of the set of state bits. In this paper we generalize it by allowing projections onto a collection of nondisjoint subsets of the state variables. We establish the advantage of having overlapping projections and present a new multiple constrain function for BDDs, to compute efficiently the approximate image during symbolic forward propagation using overlapping projections. We demonstrate the effectiveness of this new algorithm by applying it to several control modules from the I/O unit in the Stanford FLASH Multiprocessor. We also present our results on the larger ISCAS 89 benchmarks.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1996
Accession Number
ADA400403

Entities

People

  • Alan J. Hu
  • David L. Dill
  • Mark A. Horowitz
  • Shankar G. Govindaraju

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Accuracy
  • Algorithms
  • British Columbia
  • Computations
  • Computer Science
  • Computers
  • Iterations
  • Monte Carlo Method
  • Observation
  • Simulations
  • Simulators
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Computational Modeling and Simulation
  • Computer Vision.