Overview

The VAMP assembler model is the assembly-level model of the Verified Architecture Microprocessor (VAMP), a realistic RISC processor inspired by IBM's G5 architecture. In the Verisoft project, formal models for the processor and a small operating system were developed in Isabelle/HOL, and the processor model was reused for model-based generation of test programs that check whether hardware conforms to the VAMP model.^[1]

Within the Verisoft system architecture, the relevant layer is the hardware layer at the assembly level, called VAMPasm, described as the instruction set of VAMP.^[2]

State representation

The assembler state is represented by an Isabelle/HOL record ASMcoret. Register contents are integers, and register files are lists of such integers:^[3]

type_synonym regcont = int
type_synonym registers = regcont list

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

The model includes a well-formedness predicate is_ASMcore for assembler configurations. This predicate constrains the delayed program counter and program counter, requires both general-purpose and special-purpose register files to contain exactly 32 registers, and checks that register and memory cell contents are valid assembler integers.^[3]

Instruction-set model

The VAMP assembler instruction set is defined as an abstract Isabelle datatype instr. The datatype uses instruction mnemonics as constructors with corresponding operands. The evidence distinguishes instruction classes including memory data transfer, constant data transfer, register data transfer, arithmetic and logical operations, test operations, shift operations, control operations, and basic interrupts.^[4]

Examples of constructor families shown in the evidence include Ilb for memory transfer, Ilhgi for constant transfer, Imovs2i for register transfer, Iaddio for arithmetic/logical operations, Iclri for test operations, Islli for shifts, Ibeqz for control operations, and Itrap for interrupts.^[4]

Operational semantics

Instruction semantics are provided by the Isabelle function exec_instr, which maps an assembler configuration and an instruction to the configuration resulting from executing that instruction. The evidence shows cases for arithmetic, logical, and shift instructions, such as Iaddo, Iand, and Isll, each delegating to lower-level execution helpers such as arith_exec with the relevant operation.^[4]

The transition relation is defined by Step, which executes the current program instruction selected by the delayed program counter:^[4]

definition Step :: ASMcoret => ASMcoret
where Step st == exec_instr st (current_instr st)

These transition relations are used as the basis for test specifications in the cited case study.^[4]

Abstraction level

The assembler model is more abstract than the processor model. The evidence states that details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering are made transparent at this level. In the studied black-box testing scenario, the abstract model is used to generate test cases whose purpose is to check that the processor behaves as described by the assembler model, independently of internal implementation details.^[5]

Test-generation use

The case study applies two testing scenarios to VAMP processor conformance: model-based unit testing and sequence testing. Unit testing is specified with pre- and post-conditions over inputs and results, assuming control of the initial state and access to internal state after the test. Sequence testing uses sequences of system inputs and observed outputs, requiring control of state initialization and sometimes reference to the final state.^[6]

The study uses unit tests to test individual operations or instructions with different data and sequence tests to test instruction sequences up to a bounded length. The explored instruction groups are memory load/store operations, arithmetic operations, logic operations, and control-flow-related operations.^[6]

A general unit-test specification compares the system under test with the model's exec_instr result. The conformance relation _ =k _ compares register contents and only the top k memory cells rather than infinite memory. In this specification, SUT is a free variable that is replaced during test execution by the actual system under test.^[7]

Generated executable model

The Isabelle/HOL model can be used to generate executable Standard ML code. The evidence shows an SML structure VAMP containing the generated instr datatype and functions including int_add, int_sub, cell2data, exec_instr, sigma_0, and execInstrs. The instr datatype is generated from the instruction type definition, while functions are generated from corresponding constants and functions in the model.^[8]

In the reported experiment, HOL-TestGen generated two test scripts for load/store and arithmetic operation sequences. Each case produced 585 test cases, which were transformed into executable testers. When the same model was used for both test generation and execution, no errors were found.^[8]

To evaluate the generated tests, the authors introduced mutations into the generated SML model in int_add, int_sub, and cell2data. For arithmetic-operation tests, 282 of 585 tests failed; for load/store tests, 531 of 585 tests failed. The authors report these failures as detection of the introduced errors by a majority of tests.^[8]

Role in the tool chain

The case study contrasts its approach with test-generation approaches based on independently developed dedicated test models. Its stated distinction is that test-program generation is integrated into an existing Isabelle/HOL-based verification tool chain and reuses existing verification models.^[9]

References

^[1]: See citation C1. ^[2]: See citation C2. ^[3]: See citation C3. ^[4]: See citation C4. ^[5]: See citation C5. ^[6]: See citation C6. ^[7]: See citation C7. ^[8]: See citation C8. ^[9]: See citation C9.