Overview
Test Program Generation for a Microprocessor: A Case-Study is a paper by Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff. It presents a case study on generating test programs from a formal microprocessor model in order to validate that a processor implements its specified instruction set correctly. The case study uses HOL-TestGen, a model-based testing environment built as an extension of Isabelle/HOL, and applies it to the VAMP processor model. [title-authors] [case-study-purpose]
The motivation is certification of critical safety and security systems. The paper states that reaching Common Criteria EAL 7 requires formal verification of specification properties as well as thorough implementation testing, including testing of the hardware platform underlying the proof architecture. [certification-context]
Technical setting
The target of the case study is VAMP, the Verified Architecture Microprocessor. The paper describes VAMP as a realistic RISC processor model inspired by IBM's G5 architecture, developed in the Verisoft project together with a small operating-system model in Isabelle/HOL. [vamp-background]
Within the Verisoft architecture, the work focuses on the hardware layer, specifically the assembly-level instruction-set model called VAMPasm. The paper states that VAMP is a pipelined RISC processor based on out-of-order execution, and that VAMPasm contains 56 instructions across memory transfer, constant transfer, register transfer, arithmetic and logical operations, test operations, shift operations, control operations, and interrupt handling. [vamp-instruction-set]
Testing approach
The paper frames the work as model-based generation of test programs that can be used as the basis for a certification kit. Rather than developing certification test sets manually, the approach reuses the design model already used for verification. HOL-TestGen generates test sequences from the VAMP model, benefiting from the existing Isabelle/HOL verification models and proofs. [model-reuse]
The case study tests conformance between two abstraction levels: tests are generated from a formal model of the VAMP instruction set, and the conformance of the gate level to the assembly level is checked. In model-based-testing terminology used by the paper, the gate level corresponds to the implementation and the assembly level corresponds to the model. [gate-to-assembly-conformance]
The paper considers a black-box testing scenario in which an abstract system description is used for test generation. In this scenario, the processor model is used to extract abstract test cases, with the aim of checking that the processor behaves as described in the assembler model independently of implementation details such as interrupt handling, virtual memory, caching, pipelining, or instruction reordering. [black-box-abstraction]
Test scenarios
The paper develops two main testing scenarios:
- Model-based unit testing, where a test specification is described by preconditions and postconditions over inputs and outputs. In this scenario, the tester assumes control over the initial state and access to internal states after the test.
- Sequence testing, where only initialization of internal state is necessary, and in some cases the final state is referenced. The result is inferred from a sequence of system inputs and observed outputs. [unit-and-sequence]
In the case 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 studied instruction groups are memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. [instruction-groups]
HOL-TestGen role
HOL-TestGen is described as a formal tool built on top of Isabelle/HOL. It serves as a document-centric modeling environment for the background test theory, test specifications, logical transformations of test goals, and test generation. The paper summarizes its method as including test-case generation, test-data selection using constraint solving and random generation with the integrated SMT solver Z3, and a test-execution phase. [hol-testgen-method]
For unit instruction testing, the paper gives a specification pattern in which a system under test executing an instruction from an initial state is compared with the formal instruction execution function. The conformance relation compares the register contents and the top k memory cells rather than infinite memory. Each generated test case consists of an instruction, an initial configuration, and the resulting configuration after executing the instruction. [unit-specification]
Significance
The paper's contribution is to connect formal verification artifacts with test generation for processor certification scenarios. It uses formal models developed in Isabelle/HOL not only for proof but also as a basis for synthesizing executable conformance tests. The paper reports conformance test scenarios in which processor models were used to synthesize test programs run against real hardware in the loop. [case-study-purpose]