Experiments with SAT-Based Symbolic Simulation Using Reparameterization in the Abstraction Refinement Framework

Abstract

This paper presents experimental results on the performance effect of using symbolic simulation with SAT-based reparametrization within the Counter-example Guided Abstraction Refinement framework. Abstraction refinement has been applied successfully to prove safety properties of large industrial circuits. However, all existing abstraction refinement frameworks simply use SAT-based Bounded Model Checking (BMC) to refute the property. The model used for the BMC instance is not abstracted, and thus is susceptible to the state space explosion problem. We address this issue by using a symbolic simulator with a SAT-based reparametrization algorithm as a replacement for BMC within the abstraction refinement framework. The reparametrization is performed as soon as the equations maintained by the symbolic simulator become too large. We discuss the quality of the refinement information that is extracted from the symbolic simulator.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 13, 2004
Accession Number
ADA457878

Entities

People

  • Daniel Kroening
  • Edmund M. Clarke
  • Pankaj Chauhan

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Advanced Electronics
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Computations
  • Computer Science
  • Computers
  • Concrete
  • Contracts
  • Electrical Engineering
  • Engineering
  • Equations
  • Iterations
  • Machines
  • Military Research
  • Simulations
  • Simulators
  • Transitions
  • Universities

Readers

  • Database Systems and Applications
  • Operations Research
  • Quantum Dot Semiconductor Device Photonics and Graphene Optoelectronic Materials and THz Physics.

Technology Areas

  • Space
  • Space - Satellites