load and store operations Wiki

Overview

In the VAMP processor case study, load and store operations are identified as memory-related instructions within the processor's implemented DLX instruction set. The VAMP implements the full DLX instruction set, including load and store operations for double words, words, half words, and bytes, alongside shift, jump-and-link, arithmetic, and logical operations. [C1]

The processor state model used in the study includes a memory model (mm) and register files. At the ISA level, the VAMP configuration includes a 2^32-byte addressable memory model, while the assembler-level abstraction represents memory as a mapping from natural numbers to integers. [C2]

Role in the VAMP/DLX instruction set

The evidence treats load and store operations as one of four studied instruction families: memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [C3]

For test generation, the study defines a predicate is_load_store that classifies instructions as load/store operations by combining predicates for word, half-word, and byte load/store instructions:

definition is_load_store :: instr ⇒ bool
where is_load_store iw ≡ is_load_store_word' iw
        ∨ is_load_store_hword' iw
        ∨ is_load_store_byte' iw

The byte-level predicate shown in the evidence includes byte load, unsigned byte load, and byte store instruction forms such as Ilb rd rs imm, Ilbu rd rs imm, and Isb rd rs imm. [C4]

Model-based unit testing

In the unit-test scenario, the load/store predicate is introduced as a precondition so that generated tests are restricted to load and store operations. The stated test goal compares the system under test (SUT) with the abstract instruction execution function exec_instr using the executable conformance relation =k:

test_spec is_load_store ι ⇒ SUT σ0 ι =k exec_instr σ0 ι

HOL-TestGen performs exhaustive case splitting over the instruction datatype and generates symbolic operands for each instruction. For the load/store unit-test scenario, the generation produced 8 symbolic test cases corresponding to the different load and store operations, each paired with a uniformity hypothesis. [C5]

An example symbolic load test case shown in the evidence is:

SUT σ0 (Ilb ??X7 ??X6 ??X5) (...)

The subsequent test-data instantiation phase can produce a concrete test case such as:

SUT σ0 (Ilb 1 0 1) σ1

where σ1 is the expected final state after executing the operation. The evidence states that such unit-style tests can reveal design faults when an operation's result is incorrect and can also detect undesired state modifications, such as changes to flags or registers. [C6]

Sequence testing

The study also characterizes sequences of load and store instructions by applying the same is_load_store predicate to an instruction list using the HOL library combinator list_all. Instead of specifying a trace automaton or extended finite-state machine, the authors use monadic combinators of the state-exception monad to define valid test sequences. [C7]

The load/store sequence-test specification shown in the evidence is:

test_spec list_all is_load_store (ιs::instr list) ⇒
        (σ0 |=(s ← mbind ιs execVAMP; assertSE (λσ. σ =k SUT σ0 ιs)))

One generated length-3 sequence contains a word store followed by two unsigned byte loads:

[Isw ??X597 ??X586 ??X575,
 Ilbu ??X557 ??X546 ??X535,
 Ilbu ??X517 ??X506 ??X595]

After test-data instantiation, one concrete sequence is given as:

ISW   0 1  8
LLBU  1 0 -3
LLBU  3 2  8

The evidence states that such test programs can reveal errors related to read and write sequences, including byte-alignment errors and information loss due to pipelining, even when each individual operation is implemented correctly. [C8]

Observability considerations

The case study notes that checking postconditions over the final automaton state is not always realistic for hardware processors because the final state, especially internal processor registers, may not be directly observable. As an alternative, the authors describe using return for step-by-step checking of output values, such as values retrieved from updated memory cells, with a modified VAMP that exposes individual-step internal register content through trusted code. [C9]