In the VAMP (verified architecture microprocessor) project we have
designed, functionally verified, and synthesized a processor with full
DLX instruction set, delayed branch, Tomasulo scheduler, maskable
nested precise interrupts, pipelined fully IEEE compatible dual
precision floating point unit with variable latency, and separate
instruction and data caches. The verification has been carried out in
the theorem proving system PVS. The processor has been implemented on
a Xilinx FPGA.


               (                   (