Efficient Validity Checking for Processor Verification

We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessorcontrol circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description. 1 Introduction As microprocessor designs become more complex, the cost of validation becomes a larger fraction of the total design cost. Currently, validation consumes 25-30% of the design team and months of simulation time. Industry experts predict that there may soon be two or three validation engineers for every design engineer on major microprocessor design projects [Wil95]. Although today's theorem provers could be used,..