Overview

VAMP stands for Verified Architecture MicroProcessor. The provided case-study evidence characterizes VAMP as a pipelined reduced instruction set (RISC) processor based on the out-of-order execution principle. Its assembly-level instruction set is referred to as VAMPasm. [VAMP processor identity and architecture]

Within the Verisoft architecture, the cited work focuses on the hardware layer, specifically the assembly-level model of VAMP. The testing setup generates tests from a formal model of the instruction set and checks conformance of the gate level against the assembly level. [VAMP testing layer]

Instruction set

VAMPasm is described as an instruction set with 56 instructions, grouped as follows: 8 memory data-transfer instructions, 2 constant data-transfer instructions, 2 register data-transfer instructions, 14 arithmetic and logical operations, 16 test operations, 6 shift operations, 6 control operations, and 2 interrupt-handling instructions. [VAMPasm instruction inventory]

The VAMP processor is also stated to implement the full DLX instruction set from Hennessy and Patterson, including 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. [DLX implementation]

ISA-level programmer model

In the Verisoft project, an Isabelle/HOL programmer model of the VAMP processor was introduced. The model defines processor behavior as transitions over ISA configurations. A configuration contains five main elements: a program counter (pcp), a delayed program counter (dcp), general-purpose registers (gprs), special-purpose registers (sprs), and a memory model (mm). [ISA configuration]

The program counter is modeled as a 30-bit register containing the address of the next instruction to be executed. The delayed program counter is also a 30-bit register and contains the currently executed instruction; the fetch of the next instruction occurs through pcp while dcp remains unchanged until execution of the current instruction completes. The evidence identifies this as a delayed-PC pipelining mechanism. [Delayed program counter]

The general-purpose register file contains 32 registers of 32 bits each, addressed by indices 0 through 31, with the first register always set to 0. The special-purpose register file also contains 32 registers of 32 bits each and is used for tasks such as status, interrupt masks, flags, and condition registers. [Register files]

The VAMP memory interface consists of two memory management units that access instruction and data caches, which then access physical memory through a bus protocol. The VAMP system is also described as implementing caching and virtual-memory infrastructures. [Memory interface]

Assembly-level abstraction

To avoid the complexity of bit-vector representations for data and instructions, the model introduces an assembly-language abstraction of the VAMP ISA. In this assembler model, addresses are represented as natural numbers, while registers and memory contents are represented as integers. Test specifications and experiments in the cited study are based on this assembler model. [Assembler abstraction]

The Isabelle theory of the assembler model abstracts additional ISA features: instructions are represented as an abstract datatype with readable names; address translation is not visible; computations occur in a linear virtual-memory space; and interrupts are not visible at this level. [Assembler model feature abstraction]

The assembler configuration is represented by an ASMcoret record with fields for the program counter, delayed program counter, general-purpose register file, special-purpose register file, and memory model. The well-formedness predicate is_ASMcore requires both register files to contain exactly 32 registers and checks that register and memory cells contain valid values. [ASMcore representation]

Operational semantics

The assembler instruction set is defined in Isabelle as an abstract datatype instr, with operation mnemonics represented as datatype constructors associated with their operands. The instruction classes include data transfer, arithmetic and logical operations, test operations, shift operations, control operations, and basic interrupts. [Instruction datatype]

Instruction semantics are given by an exec_instr function that maps an assembler configuration and an instruction to the resulting configuration. A Step transition function is then defined by executing the current program instruction selected from the delayed program counter. These transition relations form the basis of the test specifications in the case study. [Instruction semantics]

Model-based conformance testing

The cited study uses both unit testing and sequence testing. Unit testing is used to test individual operations or instructions with different data, while sequence testing is used to test instruction sequences up to a given length. The study separately considers memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [Testing scenarios]

The assembler model is more abstract than the processor model, making details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering transparent. In the black-box testing scenario described in the evidence, the abstract model is used to generate tests that check whether the processor behaves as described by the assembler model, independently of internal implementation details. [Black-box conformance]

HOL-TestGen is used to produce tests from the specification. Each unit test case consists of an instruction, an initial configuration, and the resulting configuration after executing the instruction. The standard conformance relation compares the modeled state with the system-under-test state, including register contents and a bounded portion of memory. [HOL-TestGen conformance]