Formal Verification of Pipelined Processors using Uninterpreted Functions


Modern 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 :

©2002-2018 U.C. Regents