>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.
As Cohn's paper noted, "verification" means different things to different
people.
>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.
"Verifying" the behavior of a very simplified textbook example that
omits, for example, the complex timing that makes these things
tough is still the material of research papers.
>I have a paper on using HOL to verify a 5 stage pipeline uP (similar to
>DLX) at
Nice html document too. But it is important to note the immense
gap between a verification of an example pipeline when such issues
as setup time and interrupts are abstracted out and a
verification of an actual processor. Does your pipleline allow
forwarding? Aliasing? Branch predication?
>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.
Do you teach them to verify that the block description is an
accurate model of the lower level circuit behavior? Do you teach them
to verify correctness of interrupt operation? Do you teach them to
verify that setup times are always respected and that the memory
interface is properly designed? What does "verify" mean in this
situation?