Overview

VAMP (Verified Architecture Microprocessor) is a realistic RISC processor model inspired by IBM's G5 architecture. It was developed and verified in the German Verisoft and VerisoftXT research projects, whose verification goal covered computer systems from application-level software down to silicon-level hardware design. [VAMP origin and verification context]

Within the Verisoft architecture, work on VAMP focuses on the hardware layer, especially the assembly-level instruction-set model known as VAMPasm. The processor is described as a pipelined reduced instruction set computer based on out-of-order execution. [VAMPasm and microarchitecture summary]

Instruction set

VAMPasm is the assembly-level instruction set of VAMP and contains 56 instructions: 8 memory data-transfer instructions, 2 constant data-transfer instructions, 2 register data-transfer instructions, 14 arithmetic and logical instructions, 16 test instructions, 6 shift instructions, 6 control instructions, and 2 interrupt-handling instructions. [VAMPasm and microarchitecture summary]

The VAMP processor implements the full DLX instruction set from Hennessy and Patterson. The instruction set includes load and store operations for double words, words, half words, and bytes, as well as shift operations, jump-and-link operations, and arithmetic and logical operations. [Instruction set and assembler abstraction]

Formal processor model

An Isabelle/HOL programmer's model of VAMP was introduced in the Verisoft context. In that model, the processor is represented by transitions over Instruction Set Architecture (ISA) configurations. [ISA configuration elements and memory interface]

An ISA configuration consists of five elements:

• Program counter (pcp): a 30-bit register containing the address of the next instruction to be executed. It is used to fetch the next instruction without altering the execution of the current instruction; this pipelining mechanism is called the delayed program counter mechanism.
• Delayed program counter (dcp): a 30-bit register containing the currently executed instruction. While the next instruction is fetched through pcp, dcp remains unchanged until the current instruction completes.
• General-purpose registers (gprs): 32 registers of 32 bits each, addressable by indices 0 through 31. The first register is always set to 0.
• Special-purpose registers (sprs): 32 registers of 32 bits each for particular tasks; examples include the status register with interrupt masks and registers used as flag or condition registers.
• Memory model (mm): a 2^32-byte addressable memory, with caching and virtual-memory infrastructures implemented in the VAMP system. [ISA configuration elements and memory interface]

The memory interface of VAMP consists of two Memory Management Units that access instruction and data caches, which then access physical memory through a bus protocol. [ISA configuration elements and memory interface]

Assembly-level abstraction

To avoid complex bit-vector representations of data and instructions, an assembly language was introduced as an abstraction of the VAMP ISA. In this assembler model, addresses are represented by natural numbers, while registers and memory contents are represented by integers. Test specifications and experiments in the cited case study are based on this assembler instruction-set model. [Instruction set and assembler abstraction]

The Isabelle theory of the assembler model abstracts several ISA-level features. Instructions are represented as an abstract datatype with readable names; address translation is not visible, and assembler computations operate in a linear virtual memory space. Interrupts are also not visible at this abstraction level. [Instruction set and assembler abstraction]

The assembler configuration is represented as a record with fields for pcp, dcp, gprs, sprs, and mm, where the register files are lists of integers and memory is modeled as a mapping from natural numbers to integers. [Instruction set and assembler abstraction]

Model-based conformance testing

VAMP has been used as the subject of a case study on model-based generation of test programs. The case study adapts and reuses the Isabelle/HOL processor model to generate test cases for checking whether hardware conforms to the VAMP processor model. [Model-based conformance testing with HOL-TestGen]

The cited testing approach uses HOL-TestGen, which is built on Isabelle/HOL, to generate test sequences from the VAMP model. A stated motivation is that verification models can be reused for test generation because HOL-TestGen expresses test specifications in higher-order logic and is tightly integrated with the verification environment. [Model-based conformance testing with HOL-TestGen]

In the unit and sequence test scenarios, tests are generated from the formal instruction-set model. The conformance target is the gate-level implementation against the assembly-level model. [VAMPasm and microarchitecture summary]

The testing work distinguishes two scenarios:

1. Model-based unit testing, where tests are specified using pre- and post-conditions over inputs and results, assuming control over the initial state and access to the system-under-test state after the test.
2. Sequence testing, where tests use sequences of inputs and observed outputs, requiring control over internal-state initialization and, in some cases, reference to the final state. [Testing scenarios and conformance relation]

The case study uses unit testing to test individual operations or instructions with different data, and sequence testing to test instruction sequences up to a given length. The studied instruction categories are memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [Testing scenarios and conformance relation]

A general unit-test specification compares execution by the system under test with execution by the model function exec_instr. The conformance relation compares register contents and the top k memory cells rather than an infinite memory. [Testing scenarios and conformance relation]

Abstraction boundary

The assembler model used for test generation is more abstract than the processor model. It intentionally hides implementation details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering. In the black-box testing setting described in the case study, this abstract description is used to generate tests whose aim is to check that the processor behaves as described by the assembler model, independently of internal implementation details. [Testing scenarios and conformance relation]