Putting it all together - Formal verification of the VAMP

Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
[doi] [Google Scholar] [DBLP] [Citeseer]

International Journal on Software Tools for Technology Transfer 8(4)
Pages 411-430
01 August 2006
Note(s): ISA specification, CPU verification, PVS theorem prover

Verified an implementation of the DLX architecture against its ISA specification using PVS. The processor supported out-of-order execution using a Tomasulo scheduler, interrupts, floating point and I/D-caches.