Verifying Safety Properties of a PowerPC (Trade Mark) Microprocessor Using Symbolic Model Checking without BDDs

Abstract

In Bounded Model Checking with the aid of satisfiability solving (SAT) was introduced as an alternative to traditional symbolic model checking based on solving fixpoint equations with BDDs. In this paper we show how bounded model checking can take advantage of specialized optimizations. We present a bounded version of the cone of influence reduction that works very well for verifying safety properties. We have successfully applied this idea to checking safety properties of a PowerPC microprocessor under design at Motorola's Somerset PowerPC design center. Based on that experience, we propose a verification methodology that we feel can bring model checking into the mainstream of industrial chip design.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1999
Accession Number
ADA366208

Entities

People

  • A. Biere
  • E. Clarke
  • R. Raimi
  • Yupeng Zhu

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Circuits
  • Computer Networks
  • Computer Science
  • Computers
  • Diameters
  • Environment
  • Failure Mode And Effect Analysis
  • Governments
  • Invariance
  • Microprocessors
  • Safety
  • Sequences
  • Simulations
  • Specifications
  • Transitions
  • United States Government
  • Verification

Fields of Study

  • Computer science

Readers

  • Integrated Circuit Design and Technology.
  • Mathematical Modeling and Probability Theory.
  • Software Verification and Validation.