Main page |
| Project overview |
| We aim to formally verify the VAMP microprocessor. The VAMP is a variant of the DLX processor, a 32-bit RISC processor. The VAMP features a Tomasulo scheduler, precise and nested interrupts, a 5-stage pipeline, a fully IEEE compliant floating point unit, and a cache memory interface (with TLB). The VAMP floating point unit supports addition/subtraction, multiplication/division, comparison and type conversions. Both single and double precision numbers are supported. Denormals and exceptions are handled by the FPU as requested by the IEEE standard. Verification is done on gate level using SRI's PVS theorem prover. We develop a tool that automatically translates the PVS hardware specifications to Verilog HDL. The verified VAMP core will then be implemented on a Xilinx FPGA. |
| Project status |
| The formal verification of the VAMP-CPU wit FPU, caches, and Tomasulo core is finished using PVS 2.3 (patch level 1.2.2.36). The IEEE floating point arithmetic and the cache memory interface have been successfully verified. The translation tool PVS2HDL is finished. The VAMP has been synthesized and implemented on a Xilinx FPGA without hardware debugging in the verified parts. We run several test programs successfully.
In 2005, the VAMP has been extended with virtual memory support and address translation. The formal verification in the theorem prover PVS has also been completed. The group of Prof. Peter-Michael Seidel from SMU, Dallas, has developed the VAMPExplorer in a joint project with our institute. The VAMPExplorer is a GUI that allows intuitive access to the extensive VAMP sources. The VAMPExplorer is available online in order to allow the developers of automated methods to easily use the VAMP sources as a benchmark suite for their tools. |
| Project members |
|
Dr. Sven Beyer Dr.-Ing. Jakov Dalinger Dr. Christian Jacobi Dr. Dirk Leinenbach Prof. Dr. Wolfgang J. Paul |
