MicroTESK (Microprocessor TEsting and Specification Kit) is a framework for generating test programs in assembly language for functional verification of microprocessors. It uses formal specifications as a source of knowledge about the configuration of the microprocessor under verification. Generation tasks are described in a special Ruby-based language which allows formulating verification goals in terms of test situations derived from formal specifications. Such an approach simplifies configuring the framework and improves the level of test coverage. MicroTESK has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors.
The main approach to functional verification of microprocessors is generation of test programs and analysis of their execution traces. Functional verification is quite a laborious task which accounts for more than 70% of overall project resources. One of the reasons is difficulty related to adapting existing generators to testing new microprocessor types. In the majority of cases, a test program generator created for a specific microprocessor has to be rewritten from scratch in order to switch to a new architecture. The approach applied in the MicroTESK framework helps significantly simplify this task. It is applicable to a wide range of microprocessors (RISC, CISC, VLIW, DSP) and implies automated construction of test program generators on the basis of formal specifications of their architectures. The constructed generators consist of two main parts: (1) core that implements generation methods common for all microprocessors and (2) model that holds knowledge about a specific microprocessor. The generators create random, combinatorial and directed tests on the basis of test templates which describe test scenarios in an abstract way. Templates for directed tests are described in terms of test situations, “interesting” for testing events that occur in a microprocessor in certain conditions. Information on test situations is automatically extracted from formal specifications. Conditions for test situations are described as constraints to be solved in the process of generation. Flexible architecture of the MicroTESK framework facilitates adding support for custom generation methods.
Formal specifications are created in the nML language that allows specifying syntax and semantics of instructions skipping all unnecessary implementation details. The specifications include descriptions of the following entities: (1) storage elements such as registers and memory which characterize the microprocessor state; (2) addressing modes which provide access to storage elements; (3) instructions which update the microprocessor state by reading and writing values to storage elements. Picture 1 shows the nML specification of the ADD instruction of a MIPS microprocessor and related storage elements. Also, it shows connection between the formal specification of the instruction and its description from the MIPS architecture reference manual.
Picture 1. nML specification of the ADD instruction.
The MicroTESK framework consists of two main parts: (1) modeling framework and (2) testing framework. The first is responsible for constructing microprocessor model on the basis of formal specifications. The aim of the second is generating test programs on the basis of the model and test templates. Components of the MicroTESK framework are shown in Picture 2.
Picture 2. Components of MicroTESK.
Modeling framework is represented by an extensible set of specification analyzers and code generators. The constructed model includes: (1) metadata that stores information about supported registers and instructions; (2) simulator that executes instructions in order to track the microprocessor state; (3) coverage model that contains a catalogue of test situations.
Generation framework constructs test programs on the basis of test templates describing generation tasks at an abstract level where instructions being used, their order and their arguments are not fixed, but selected dynamically depending on the formulated task. The process of generation includes the following stages:
1. Analysis of a test template and construction of abstract instruction sequences;
2. Enumerating abstract sequences and performing the following actions for each of them:
- sequence concretization: register selection, data generation, construction of initialization code;
- execution of instructions on the simulator;
- construction of self-checks on the basis of state information provided by the simulator;
- adding the sequence into the instruction stream.
3. Splitting the instruction stream into programs and printing them in the assembly format.
Picture 3 shows a test template that describes pairs of ADD and SUB instructions causing situations IntegerOverflow (integer overflow exception) and Normal (no exceptions) in all possible combinations and an example of a test case constructed on its basis.
Picture 3. Test template and test case constructed on its basis.
More information can be found here.