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
               (
geocities.com/de/christian_jacobi)                   (
geocities.com/de)