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

摘要

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.