| |
|
|
Formal Verification of Pipelined Processors using Uninterpreted FunctionsAbstractModern microprocessors utilize complex pipelining schemes to achieve high performance while preserving the illusion that instructions are executed in sequential order. Processor design teams typically employ more people performing validation, consisting largely of running simulations to find bugs in the pipelining logic, than they do in creating the designs. We consider the problem of formally verifying that a pipelined processor has behavior matching that of an unpipelined, instruction set reference model, effectively proving the absence of any pipelining bug. We abstract the operation of the processor datapath as a set of uninterpreted functions and uninterpreted predicates operating on abstract data. Using the symbolic pipeline flushing technique of Burch and Dill, verification reduces to deciding the validity of a formula in a logic of equality with uninterpreted functions. We have developed methods to reduce formulas in this logic into propositional logic that take advantage of the properties of the formulas generated when modeling microprocessors. We have been able to verify several single- and dual-issue pipelines, including ones implementing exception handling. We have experimented with both Binary Decision Diagrams and Boolean satisfiability checkers, on both good and buggy circuits. Our results are the best achieved by anyone to date for automated pipeline verification, although we are still well short of the goal of handling state-of-the-art microprocessors.
Relevant Papers :
Logic of Equality With Uninterpreted Functions,'' Computer-Aided Verification CAV '99, N. Halbwachs, and D. Peled eds., LNCS 1633, Springer-Verlag, July, 1999, pp. 470-482. Available as http://www.cs.cmu.edu/~bryant/pubdir/cav99a.ps. Reductions of the Logic of Uninterpreted Functions to Propositional Logic,'' Technical Report CMU-CS-99-115, May, 1999. Available as http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-115.ps, and also as http://www.cs.cmu.edu/~bryant/pubdir/CMU-CS-99-115.ps. Efficient Reductions of the Logic of Equality with Uninterpreted Functions,'' Correct Hardware Design and Verification Methods CHARME '99, September, 1999. Available as http://www.cs.cmu.edu/~bryant/pubdir/charme99.ps. |