Definition
The assembler model is an Isabelle/HOL theory that abstracts the instruction-set architecture used for the VAMP processor case study. It was introduced to avoid the complexity of bit-vector representations of data and instructions: addresses are represented as natural numbers, while register contents and memory contents are represented as integers. Test specifications and experiments in the case study are based on this instruction-set, or assembler, model. [C1]
Abstraction level
The model abstracts several ISA and processor-level details. Instructions are represented as an abstract datatype with readable constructor names, address translation is not visible, assembler computations take place in a linear virtual memory space, and interrupts are not visible at this level. The assembler model is described as more abstract than the processor model, making complex details transparent, including interrupt handling, virtual memory and caching, pipelining, and instruction reordering. [C2]
Configuration state
The assembler configuration is an abstraction of the ISA configuration and is defined as the ASMcoret record type. Its fields are:
pcp: a natural number representing the program counter.dpc: a natural number representing the delayed program counter.gprs: a list of integers representing the general-purpose register file.sprs: a list of integers representing the special-purpose register file.mm: a memory model represented by a mapping from naturals to integers. [C3]
The register-file type is defined as a list of integers. Because the assembler representation is less restrictive than the bit-vector representation, predicates and conversion functions restrict addresses, values, and configurations to meaningful values. The well-formedness predicate is_ASMcore ensures that both register files contain exactly 32 registers and that register and memory cells contain valid values. [C4]
Instruction representation and semantics
The assembler instruction set is defined in Isabelle as an abstract datatype instr. Operation mnemonics are datatype constructors with their associated operands. The instruction classes shown in the evidence include data-transfer commands, arithmetic and logical operations, test operations, shift operations, control operations, and basic interrupts. [C5]
Instruction semantics are provided by exec_instr, a function over assembler configurations and assembler instructions. For each configuration and instruction, it returns the resulting configuration after executing the instruction in the initial configuration. The transition relation is defined by Step st ≡ exec_instr st (current_instr st), so a transition maps a configuration to its successor by executing the current instruction indicated by the delayed program counter. [C6]
Role in testing
The transition relations of the assembler model are used as the basis of test specifications. In the black-box testing scenario described in the case study, an abstract description of the system under test is used for test generation, with the goal of checking that the processor behaves as described in the assembler model independently of internal implementation details. [C7]
For unit instruction testing, a general specification compares the system under test with the assembler execution function:
test_spec pre σ ι ⇒ SUT σ ι =k exec_instr σ ι
Here =k is an executable conformance relation comparing registers and the top k memory cells rather than infinite memory. Each test case consists of an instruction, an initial configuration, and the resulting configuration after executing the instruction. HOL-TestGen produces tests from this specification, and subsets of instructions can be isolated by adding preconditions that specify the instruction type. [C8]
Tested instruction categories
The case study applies both model-based unit testing and sequence testing. Unit testing is used to test each operation or instruction with different data, while sequence testing is used for sequences of instructions up to a given length. The studied instruction categories are memory-related load and store operations, arithmetic operations, logic operations, and control-flow-related operations. [C9]