VAMP ISA Wiki — STIMSMITH

Overview

The VAMP ISA is the instruction-set architecture level used in the formal VAMP processor model described in the Verisoft context. The Isabelle/HOL programmer’s model defines the VAMP processor as transitions over ISA configurations. A separate assembler model abstracts the ISA to avoid lower-level bit-vector representations of data and instructions, and the cited case study uses this assembler model as the basis for test specifications and experiments. [isa-programmers-model]

The VAMP processor is described as implementing the full DLX instruction set from Hennessy and Patterson. The supported instruction set includes load and store operations for double words, words, half words, and bytes, along with shift operations, jump-and-link operations, and arithmetic and logical operations. [dlx-coverage]

ISA configuration

At the ISA level, a VAMP configuration is composed of five elements: [isa-configuration]

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 execution of the current instruction.
Delayed program counter (dcp) — a 30-bit delayed-program-counter register associated with the currently executed instruction. While the next instruction is fetched through pcp, dcp remains unchanged until the current instruction finishes.
General-purpose registers (gprs) — 32 registers of 32 bits each, addressable by index 0–31. The first register is always set to 0.
Special-purpose registers (sprs) — 32 registers of 32 bits each, used for particular tasks such as interrupt masks, flags, and condition registers.
Memory model (mm) — a 2^32-byte addressable memory model; the VAMP system also includes caching and virtual-memory infrastructure.

Assembly-level abstraction

The assembler model is an abstraction of the VAMP ISA. It represents addresses as natural numbers and register and memory contents as integers. Instructions are represented by an abstract datatype with readable constructor names. At this level, address translation is not visible, assembler computations operate in a linear virtual memory space, and interrupts are not visible. [assembler-abstraction]

The assembler configuration is represented by the Isabelle/HOL record ASMcoret. Register files are modeled as lists of integers: [asmcoret-record]

type_synonym regcont = int           -- {* contents of register *}
type_synonym registers = regcont list -- {* register file *}

record ASMcoret = dpc :: nat
                pcp  :: nat
                gprs :: registers
                sprs :: registers
                mm   :: memt

Because the assembler representation of addresses and values is less restrictive than the bit-vector representation, the model defines well-formedness constraints. The is_ASMcore predicate checks that dpc and pcp are valid assembler natural values, that the general-purpose and special-purpose register files each contain exactly 32 registers, and that register and memory cells contain valid values. [well-formedness]

definition is_ASMcore :: ASMcoret ⇒ bool where
 is_ASMcore st ≡ asmnat (dpc st) ∧
        asmnat (pcp st) ∧
        length (gprs st) = 32 ∧
        length (sprs st) = 32 ∧
        (∀ ind < 32. asm_int (reg (gprs st) ind)) ∧
        (∀ ind < 32. asm_int (sreg (sprs st) ind)) ∧
        (∀ ad. asm_int (data_mem_read (mm st) ad))

Instruction representation

The assembler instruction set is defined as an abstract Isabelle datatype named instr. Operation mnemonics are modeled as datatype constructors with their operands. The evidence distinguishes data-transfer commands, arithmetic and logical operations, test operations, shift operations, control operations, and basic interrupt instructions. [instr-datatype]

Examples shown in the evidence include memory-transfer, constant-transfer, register-transfer, arithmetic/logical, test, shift, control, and interrupt constructors: [instr-datatype]

datatype instr =
  Ilb regname regname immed
| Ilhgi regname immed
| Imovs2i regname regname
| Iaddio regname regname immed
| Iclri regname
| Islli regname regname shift_amount
| Ibeqz regname immed
| Itrap immed
| ...

The case study also defines load/store test purposes over this syntax. For byte load/store instructions, the evidence gives constructors such as Ilb, Ilbu, and Isb; the overall is_load_store predicate is defined as a disjunction of word, half-word, and byte load/store predicates. [load-store-test-purpose]

Semantics and transitions

Instruction semantics are given by exec_instr, a function from an assembler configuration and an instruction to the resulting assembler configuration. The evidence shows cases for arithmetic, logical, and shift instructions, with cases delegating to helper operations such as arith_exec. [exec-instr]

fun exec_instr :: [ASMcoret, instr] ⇒ ASMcoreₜ
where
  exec_instr st (Iaddo RD RS1 RS2) =
      arith_exec st int_add (reg (gprs st) RS1)
        (reg (gprs st) RS2) RD
| exec_instr st (Iand RD RS1 RS2) =
      arith_exec st s_and (reg (gprs st) RS1)
        (reg (gprs st) RS2) RD
| exec_instr st (Isll RD RS1 RS2) =
      arith_exec st sllog (reg (gprs st) RS1)
        (reg (gprs st) RS2) RD
| ...

The assembler transition function Step returns a successor configuration by executing the current instruction, which is obtained from the delayed program counter. [step-transition]

definition Step :: ASMcoret ⇒ ASMcoreₜ
where Step st ≡ exec_instr st (current_instr st)

Role in test generation

The cited work uses the VAMP assembler model as an abstract basis for model-based conformance testing. The goal is to check that the processor behaves as described by the assembler model independently of internal implementation details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering. [testing-goal]

Two testing scenarios are described: unit testing of individual instructions with different data, and sequence testing of instruction sequences up to a given length. The study focuses on four instruction families: memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [testing-scenarios]

For unit instruction testing, the paper presents a specification of the form test_spec pre σ ι ⇒ SUT σ ι =k exec_instr σ ι, where the conformance relation compares register contents and the top k memory cells rather than infinite memory. Each generated test case consists of an instruction, an initial configuration, and the resulting configuration after executing the instruction. [unit-testing]

For sequence testing, execVAMP lifts exec_instr into the state-exception monad: [execvamp]

definition execVAMP where
  execVAMP ≡ (λ i σ. Some ((), exec_instr σ i))

The same sequence-testing setup uses preconditions, also called test purposes, to restrict generated instruction sequences to chosen subsets. Because arbitrary generated initial configurations may be ill-formed under the abstract assembler representation, the study uses an empty initial configuration σ0 that is proved to be well-formed. [sequence-testing]

VAMP ISA