Overview

In the VAMP microprocessor case study, arithmetic operations are one of the instruction categories considered for conformance testing. The VAMP implements the full DLX instruction set, which includes load/store operations, shift operations, jump-and-link operations, and various arithmetic and logical operations. [C1]

The study uses an assembler-level abstraction of the VAMP instruction set to avoid direct bit-vector representations. In this abstraction, addresses are represented as natural numbers, while registers and memory contents are represented as integers. [C2]

Place in the testing approach

The case study applies two main testing scenarios: model-based unit testing and sequence testing. Unit testing is used to test each operation or instruction individually with different data, while sequence testing is used to test instruction sequences up to a given length. The authors studied four instruction categories separately: memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [C3]

For arithmetic operations specifically, the test purpose predicate is_arith is used to constrain generated tests to arithmetic instructions. The unit-test specification shown in the study is:

test_spec σ= exec_instr σ0i =⇒is_arith i =⇒SUT σ0i σ
apply (gen_test_cases 0 1 SUT)
store_test_thm  arith_instr

Under this setup, each arithmetic operation is covered by one generated test case. The paper gives an example test case containing Iaddi, described as a test case for an addition operation. [C4]

Test granularity

The study notes that HOL-TestGen applies a fairly coarse granularity to arithmetic-operation tests in this model: for an integer variable, it selects just one value satisfying the constraints. This is attributed both to the model’s representation of registers as integers rather than 32-bit words and to HOL-TestGen’s heuristic of selecting one candidate per variable. [C5]

The suggested workaround is to refine the test-purpose definitions with additional case distinctions, so that test selection must find solutions for finer-grained constraint classes. [C5]

Sequence testing example

Arithmetic operations are also used in sequence testing. The sequence-test specification constrains an instruction list with list_all is_arith and checks conformance between the model execution and the system under test after executing the sequence. [C6]

One generated arithmetic sequence is:

ISUB  2 1 0
IADD  1 5 2
IADD  1 0 4

The study states that this sequence corresponds to a subtraction followed by two addition operations. [C7]

Role in processor conformance

Within the broader conformance-testing setting, arithmetic-operation tests are part of checking that the processor behaves according to the assembler model independently of internal implementation details. The assembler model abstracts away details such as interrupt handling, virtual memory and caching, pipelining, and instruction reordering. [C8]