Symbolic verification of the Torch instruction fetch unit: A reality check

Abstract

Last year, our group at Stanford undertook to test some of our ideas about microprocessor verification on the Stanford Torch microprocessor. Torch is a microprocessor designed by Prof. Mark Horowitz's group at Stanford; it is a testbed for some architectural ideas and an example for teaching. It has never been fabricated, but at least it was designed by designers, not verification people, and there exists Verilog and a simulation framework.

The result was NOT a straightforward application of our verification techniques. First, we had to modify tools because we were working directly on the Verilog HDL. Among other things, this required inventing an efficient decision procedure for bit vectors. When we decided to stop, we had partially verified the instruction fetch unit, and discovered several bugs. We also learned a lot about the problems, if not the solutions, of specifying units within a large design and finding inductive invariants.