Overview

In the VAMP microprocessor case study, conformance testing is framed as checking that a processor behaves as described by an abstract assembler model, independently of internal implementation details. The study uses an abstract description of the system under test as the basis for test generation in a black-box testing scenario. In the hardware-layer setting, tests are generated from the formal assembly-level instruction-set model and used to test the conformance of the gate level to the assembly level. [C1]

Conformance relation

The study defines a standard conformance relation, written _ =k _, for comparing the state controlled according to the model with the state controlled by the system under test (SUT). This executable equality compares register contents and only the top k memory cells rather than infinite memory. The approach relies on a testability assumption: the test environment is trusted to read the external state and convert it to the corresponding abstraction. [C2]

A representative unit-instruction test specification is:

test_spec pre σ ι ==> SUT σ ι =k exec_instr σ ι

Here, SUT is a free variable replaced during test execution with the actual system under test, while exec_instr represents the model-side instruction execution. [C2]

Unit and sequence testing

The case study applies two main scenarios: model-based unit testing and sequence testing. In unit testing, the test specification is described by preconditions and postconditions over the inputs and results produced by the SUT; this assumes control over the initial state and access to the SUT's internal state after the test. In sequence testing, control of internal state initialization is necessary, and in some cases the final state is referenced; test results are inferred from sequences of system inputs and observed outputs. [C3]

In the study, unit testing is used to test individual operations or instructions with different data, while sequence testing is used to test instruction sequences up to a given length. The investigated instruction groups include memory-related load/store operations, arithmetic operations, logic operations, and control-flow operations. [C3]

Test cases and test purposes

Each unit test case is composed of an instruction, an initial configuration, and the resulting configuration after executing the instruction. From the general test specification, HOL-TestGen produces tests for possible instructions. Subsets of instructions are isolated by adding preconditions to the test specification that specify the instruction type. [C4]

For sequence testing, the study distinguishes scenarios that observe local execution steps from those that test the final state. Because the local steps in the application domain are actions that do not report computation results, the final-state scenario is the relevant one. The final-state check may compare conformance over the entire state or only part of the state, such as comparing the final value of register 0 after a load. Preconditions, also called test purposes, reduce generated instruction sequences to a specified subset. [C5]

Role of model-based test generation

The study's conformance-testing setup is model-based: tests are generated from a formal model of the instruction set. HOL-TestGen, built on Isabelle/HOL, is used for stating and transforming test goals and generating tests. Its method includes a test-case generation phase, a test-data selection phase using constraint solvers, random test generation, and the SMT solver Z3, and a test-execution phase that converts instantiated test cases. [C6]

Contrast with stuck-at-fault testing

The paper contrasts its specification/model-based testing approach with stuck-at-fault techniques. Stuck-at-fault analysis modifies a circuit design through mutators that capture a fabrication fault model, such as broken wires connecting gates. The paper characterizes this as a white-box mutation technique. It notes that stuck-at-fault techniques are effective for medium-size circuits and use design structure to construct equivalence-class tests that directly incorporate a fault model, but they may not reveal design flaws such as write-read errors under byte-alignment effects in memory. [C7]