{'fraction_non_alphanumeric': 0.022693997071742314, 'fraction_numerical': 0.004392386530014641, 'mean_word_length': 5.213636363636364, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formal Verification of the VAMP Microprocessor Project Status

Microprocessors are in use in many safety-critical environments, such as cars or planes. We therefore consider the correctness of such components as a matter of vital importance. Testing microprocessors is limited by the huge state space of modern microprocessors. We therefore think formal verification is the sole way to obtain a correctness guarantee. At Saarland University, we are currently working on a project aiming to formally verify the correctness of a complete microprocessor called VAMP. The VAMP (Verified Architecture Microprocessor) is a variant of the DLX processor [11]. It features a Tomasulo-scheduled 5-stage pipeline, precise interrupts, delayed branch, virtual memory management, cache memory, and a fully IEEE compliant dual-precision floating point unit that handles denormals and exceptions entirely in hardware. The specification and verification is performed on the gate level using the PVS theorem proving system [25]. Our group has developed a tool which automatically translates hardware specifications from the PVS language to Verilog HDL. This enables us to translate the VAMP to Verilog and synthesize it on a Xilinx FPGA [7]. This paper provides an overview of the VAMP project. We sketch the proof techniques used in the verification of the different VAMP components.