control-flow operations

Definition in the VAMP case study

The provided evidence identifies control-flow related operations as one of four instruction categories studied in model-based conformance testing of the VAMP processor, alongside memory-related load/store operations, arithmetic operations, and logic operations.[C1] At the VAMP assembly level, the VAMPasm instruction set contains 56 instructions, including 6 instructions for control operations.[C2]

The same case study discusses these operations under the heading “Testing Control-Flow Related Operations” and treats them operationally as branching operations selected by a predicate such as is_branch.[C3]

Architectural context

The VAMP processor model includes program-counter state that is directly relevant to control flow. Its Instruction Set Architecture configuration includes:

• pcp, a 30-bit program counter containing the address of the next instruction to be executed;
• dcp, a delayed program counter containing the currently executed instruction.[C4]

The evidence explains that pcp is used to fetch the next instruction without altering the current instruction’s execution, while dcp remains unchanged until the current instruction finishes; this pipelining mechanism is called delayed pc.[C4]

At the assembler-model level used for test generation, the configuration abstracts these fields as natural numbers: pcp represents the program counter and dcp represents the delayed program counter.[C5]

Relationship to the instruction set

The VAMP implements the full DLX instruction set from Hennessy and Patterson as described by the case study. The evidence states that this instruction set includes load/store operations, shift operations, jump-and-link operations, and arithmetic and logical operations.[C6] In the VAMPasm categorization, control operations are counted separately as 6 of the 56 assembly-level instructions.[C2]

Model-based testing role

The case study uses an abstract assembler model as the basis for black-box test generation. The aim is to check that the processor behaves as described by the assembler model, independently of internal implementation details such as interrupts, virtual memory, caching, pipelining, and instruction reordering.[C7]

For unit testing of control-flow related operations, the study uses a specification of the following form:

test_spec is_branch i =⇒ SUT σ0 i =k exec_instr σ0 i
apply (gen_test_cases 0 1 SUT)
store_test_thm branch_instr

This generates unit test cases for branching operations from the initial state σ0.[C3]

A schematic generated unit test case shown in the evidence is:

SUT σ0 (Ijalr ??X27X7) (...)

The study notes a limitation of this fixed-initial-state scenario: branching behavior depends essentially on flag values, so a more interesting scenario would vary initial states and change flag values for each test case.[C3]

Sequence testing

The case study also gives a sequence-test specification for lists of branching instructions:

test_spec list_all is_branch (ιs::instr list) =⇒
        (σ0 |=(s ←mbind ιs execVAMP; assertSE (λσ. σ=k SUT σ0 ιs)))
apply (gen_test_cases SUT)
store_test_thm branch_instr_seq

This specification checks conformance after executing a sequence of branch instructions from the initial state.[C3]

An example generated concrete sequence is:

σ0 |=(s ←mbind [Ij 1, Ijalr 0] execVAMP;
        assertSE (λσ. σ=k SUT σ0 [Ij 1, Ijalr 0]))

The corresponding assembly sequence is:

IJ        1
IJALR     0

This example demonstrates that control-flow related tests can be generated as instruction sequences, not only as single-instruction unit tests.[C3]

Test-data generation considerations

For the scenarios considered in the study, test-data generation is performed using constraint solving and random instantiation.[C8] The paper notes that additional constraints can be added to reduce the uniformity domain and improve coverage by dividing it into more interesting sub-domains.[C8]