In our previous paper 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.

17 pages

*ILKD, University of Karlsruhe, Postfach 6980, 76128 Karlsruhe, Germany.
**Motorola, Inc., Somerset Power PC Design Center, 6200 Bridegepoint Parkway, Bldg 4, Austin, TX 78759, and Computer Engineering Research Center, University of Texas at Austin, Austin, TX 78730.

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu