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 (jrb@cadence.com) 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
ftp://lal.cs.byu.edu/pub/hol/lal-papers/pipeline.ps.gz
(In HTML at http://lal.cs.byu.edu/people/windley/papers/pipeline/pipeline.html)
Tahar (tahar@ira.uka.de) 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,
--phil--
__________________________________________________________________________
Phillip J. Windley, Asst. Professor | windley@cs.byu.edu
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="http://lal.cs.byu.edu/people/windley/windley.html">here</A> or<A
HREF="http://www.imall.com/homepage.html">here</A>.