Granted.
| "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.
Certainly, and I didn't claim that there was no more left to do. I merely
pointed out that 6 year old work wasn't the state of the art.
| 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?
Yes, yes, and see Mike Coe's thesis (in
ftp://lal.cs.byu.edu/pub/hol/lal-papers) for the third. Interrupts are
are also covered in Mike's work.
| 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?
The word verify *is* imprecise. One needs to talk about correctness
models in detail. In this stiuation it means that the RTL description of
the electronic block model correctly implements the instruction set
semantics. Going below the EBM is important and a number of people
(including us) are working on this.
As I said before, I'm not claiming that everything has been worked out, but
I do think that there are problems that can be solved now. Miriam Leeser
(of Cornell) has been doing work on verifying hardware much like the FP
hardware that caused the bug in the Pentium. I don't think that finding
such bugs is beyond the state of the art.
--phil--