We use the theorem proving system PVS to design and formally verify the
\emph{VAMP}, a 32-bit DLX-like microprocessor with out-of-order scheduler and
IEEE compliant FPU. We show that the gate level design adheres to a high level
specification. The hardware is synthesized by converting the PVS language to
Verilog. This paper provides a project overview.


--- This abstract is not part of the paper