Symbolic verification of the Torch instruction fetch unit: A reality check
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.
|©2002-2018 U.C. Regents|