Computer Science Department
School of Computer Science, Carnegie Mellon University
Verifying Safety Properties of a PowerPCTM Microprocessor Using
Symbolic Model Checking without BDDs
Armin Biere*, Edmund Clarke, Richard Raimi**, Yunshan Zhu
Keywords: Hardware verification, out-of-order execution, temporal
logic, symbolic model checking, boolean satisfiability
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.
*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.