MicroTESK

MicroTESK is a specification-based test program generation (TPG) framework for microprocessor verification. It is described in the literature as one of the few open-license tools in its class and as an open-source, extensible, reconfigurable TPG framework developed by the MicroTESK team at ISP RAS.[1][2]

Architecture and inputs

MicroTESK separates an architecture-independent test generation core from architecture-specific models. In the MIPS64 MMU work, the tool is described as consisting of a reusable generation core plus MIPS64 memory-subsystem specifications; the same paper contrasts this separation with industrial TPG systems such as IBM Genesys-Pro while emphasizing differences in specification representation and use.[3]

For MicroTESK version 2.3 and later, the main inputs are:

• ISA specifications written in a dialect of nML;
• MMU specifications written in MMUSL;
• test templates written in Ruby.[1]

The specifications are analyzed to extract testing knowledge, including execution situations and inter-instruction dependencies. That information is then used to generate test programs from user-provided test templates and to support systematic enumeration of templates.[1]

ISA and MMU specification model

ISA specifications define data types, constants, registers, access modes, memories, and instructions. The cited MIPS64 example shows register arrays, register-access modes with assembly syntax and binary image definitions, and instruction actions such as load/store behavior over a memory array.[4]

Because nML is described as too simple to adequately model MMUs, MicroTESK uses MMUSL for memory-management features. MMUSL specifications include address types, memory segments, buffers such as TLBs and caches, and control logic for handling loads and stores. Buffers can be described by associativity, number of sets, entry format, index and tag functions, and eviction policy.[4][5]

Test program generation approach

MicroTESK test templates are Ruby classes based on the framework's template library. Templates can refer to modes and instructions from the specifications and use TPG constructs such as blocks and situations. In the MIPS64 MMU example, a template block containing load and store instructions is processed by a memory engine, while a situation such as an L1 cache hit guides generation by constraining MMU variables and buffers.[5]

For MMU-oriented generation, parsing the specifications produces an interpreter for the instruction set simulator and a symbolic representation as a labeled directed acyclic graph. MicroTESK traverses the graph to extract execution paths for memory requests; paths end in memory access or exceptions such as alignment faults or TLB refill events. The tool can also derive dependencies between execution paths over shared buffers, including conflict types such as same buffer index, same tag, and recently evicted tag.[6]

Given a test template, MicroTESK enumerates symbolic test programs by selecting relevant execution paths and satisfiable dependencies. To manage combinatorial explosion, it uses heuristics including path factorization and limiting dependency depth. Symbolic programs are then instantiated with test data such as addresses, buffer entries, and load/evict sequences, and finally transformed into ISA-specific preparation code that initializes registers, buffers, and memory.[6][7]

MIPS64 MMU case study

A 2016 case study used MicroTESK to generate test programs for MIPS64 memory management units. The approach combined ISA specifications in nML with MMU specifications in MMUSL, and relied on symbolic execution and constraint solving for test-data generation.[2]

In that case study, the MIPS64 MMU specification covered address spaces, TLB entry format, address translation, and a two-level write-through cache. The MMUSL description was reported to be about 220 lines and included JTLB and DTLB TLBs, L1 and L2 cache buffers, and memory segments such as kseg0, kseg1, xkphys, and useg. Based on the ISA and MMU specifications, the authors defined 18 memory-access instructions plus auxiliary instructions for TLB and cache access.[8]

The same study notes practical limitations: exhaustive enumeration works only for very short test templates, while more complex cases require heuristics or constrained random generation. The authors also identified constraint-solving performance as a priority for further optimization and suggested extending the approach to multicore designs and multiprocessor systems.[2][8]

Project members

The public MicroTESK project page lists Alexander Kamkin as project creator and lists Alexander Kamkin and Alexander Protsenko as managers. It also lists Alexander Protsenko, Alexander Kamkin, Mikhail Chupilko, and Sergey Smolov among the project developers.[9]