Re: The Pentium chip wasn't verified

Phil Windley (
Mon, 21 Nov 1994 07:51:28 -0700

On Sun, 20 Nov 1994 12:30:08 -0700 Victor Yodaiken writes
| The state of the art is, in a word, weak.
| The Avra Cohn paper on the Viper chip is recommended
| reading for anyone with illusions about the subject. For certain small
| parts of the operation of some circuits, automated model checking has
| some indications of being useful. Automated theorem proving is more
| of a problem.

The state of the art has progressed significantly since Avra's paper.
Avra's work was state of the art for 1988. Much has changed. A number of
people are now routinely verifying pipelined uP's as complex as the MIPS
R2000. Superscalar pipeline verifications are on the horizon.

For an excellent paper about verifying uP's using model checking
technology, see Burch's ( paper in CAV94. He has verified
the DLX uP from Hennesey and Patterson.

I have a paper on using HOL to verify a 5 stage pipeline uP (similar to
DLX) at

(In HTML at

Tahar ( and Kumar (Karlsruhe) have verified the DLX uP.

As I said, if your conception of the state of the art in uP verifiction is
VIPER, you're out of date. uP's far beyond VIPER in complexity can now be
verified with little problem. I routinely teach a class of graduate
students (with no previous verification experience) how to verify uP's as
complex as VIPER in a semester.

Best Regards,


Phillip J. Windley, Asst. Professor |
Laboratory for Applied Logic |
Dept. of Computer Science, TMCB 3370 |
Brigham Young University | Phone: 801.378.3722
Provo UT 84602-6576 | Fax: 801.378.7775
If you use WWW, I can be found <A
HREF="">here</A> or<A