The basic approach is described in more detail in the paper
"Automatic Verification of Pipelined Microprocessor Control,"where we used the method to verify a version of the toy DLX processor from Hennessey and Patterson's "Computer Architecture: A Quantitative Approach." The approach uses an abstraction function to relate a detailed implementation description to a simpler specification description. HDL descriptions of the design can be symbolically simulated. The symbolic simulator manipulates symbolic states which assign an expression to each state variable in the description. Given symbolic inputs (an expression for each input variable), the symbolic simulator produces new symbolic outputs and a new symbolic state.
Jerry R. Burch and David L. Dill.
International Conference on Computer-Aided Verification, LNCS 818, Springer-Verlag, June 1994.
In the simplest case, verification requires proving a theorem.
Suppose IMPL(s,i) is a function representing the execution of one step
of the implementation, which produces a new implementation state,
SPEC(s, i) is the corresponding next-state function for the
specification, and ABS(s) is an abstraction function which maps
implementation states to specification states.
The desired property is:
Since the IMPL, SPEC, and ABS can all be written in an HDL (Verilog or our Lisp HDL), symbolic states representing the left- and right-hand sides of this equation can be generated using the symbolic simulator. A separate equation generated for each state variable. If these equations are all valid, the implementation implements the specification (precisely defining and proving this claim requires a number of other conditions).
The descriptions and symbolic simulator all work so that the expressions assigned to the state variables are in a quantifier-free fragment of first-order logic with equality and uninterpreted functions. The validity problem is decidable in this logic. We have a separate program for checking validity, which is invoked for equations generated by the symbolic simulator. If the equations are valid, the validity checker reports the result; if not, it prints a set of assumptions which are sufficient to falsify the equation. These assumptions can be extremely useful for diagnosing the problem (it may be an error in the implementation, specification, or abstraction function).
Writing an abstraction function by hand can be very time-consuming. Fortunately, there are tricks that can be used with pipelined processors to help generate an abstraction function mostly automatically.
The abstraction function basically matches up implementation states with the specification states they "simulate". The major difficulty in defining the abstraction function for a pipelined processor is dealing with partially executed instructions - at any time, there may be several instructions in the pipeline which have been executed to varying degrees. Results from these instructions will be sitting around in various pipe registers, waiting to be stored to the visible state of the processor. The abstraction function must assemble all these partial results into a meaningful visible state.
The trick we use is to generate the abstraction function by symbolically simulating the processor. Most processors have a state or input that causes them to stall, meaning that they do not issue new instructions but continue to work on the old instructions (hardware can be added to the design to add a stalling capability, if necessary). If a processor is stalled for enough cycles, all of the partially executed instructions will eventually be fully executed. A direct comparison between the implementation and visible state is then much simpler to describe.
The preceding description is vastly oversimplified, although it almost works as described for the DLX processor in Hennessey and Patterson's "Computer Architecture: A Quantitative Approach." There are two complications: invariants are needed, and input matching may be required.
The preceding use of abstraction functions requires that every implementation state properly match a specification state. This requirement is too strong, because not all implementation states can reasonably occur. The solution is to define a logical property, called an invariant that specifies which states are reachable. Invariants can be proved using the same decision procedure that is used for verifying the abstraction function. Right now, invariants must be defined manually, although we are working on ways to help automate the process of defining them.
It may also be necessary to match the inputs of the specification and implementation to get a reasonable comparison. For example, the DLX implementation may stall because of an external stall signal, or because of an internal conflict. The stall input of the specification must combine both of these conditions (it is the logical OR of the external stall for the implementation and some internal signals of the implementation).
The most ambitious project we have taken on was the verification of an (abstracted version of) the Flash Protocol Processor (PP). The PP is a dual-pipeline VLIW machine designed to provide message handling in the FLASH multiprocessor being designed at Stanford (PP is part of the MAGIC chip). This project used the basic method described above. In order to do it, we had to prove the CPU and memory system separately. The most difficult aspect of the project was finding invariants, which was done by trial and error: proofs would fail because the invariants weren't strong enough. Examining the reason for the failure provided clues about how to strengthen them. Later, we discovered a method for finding some of the necessary invariants automatically, and wrote a paper on the subject:
"Automatic Generation of Invariants in Processor Verification,"During most of this project, we used a decision procedure for quantifier-free first order formulas with equality, uninterpreted functions, and arrays. This program was written primarily by Jerry Burch, and had many high-level heuristics. Later in the project, we used a decision procedure written in C++, which obtained similar speed using simpler heuristics, but emphasizing efficiency in the low-level algorithms and data structures. The implementation was described in:
by Jeffrey X. Su, David L. Dill and Clark Barrett.
FMCAD'96, November, 1996.
"Efficient Validity Checking for Processor Verification,"Since then, the program was largely reimplemented by Clark Barrett and Jeremy Levitt, and given the name "SVC." In addition to efficiency improvements, it has a real implementation of congruence closure, linear arithmetic, and bitvectors. There is a paper describing SVC, also:
by Robert B. Jones, David L. Dill, and Jerry R. Burch.
International Conference on Computer-Aided Design, 1995.
"Validity Checking for Combinations of Theories with Equality,"An on-line demonstration of this program is also available.
by Clark W. Barrett, David L. Dill, Jeremy R. Levitt.
FMCAD'96, November, 1996.
We are currently working on verification of another processor design. Much of our effort is going into improving the level of automation, so that we don't have to spend so much time translating verilog, discovering invariants, etc.