MicroTESK
ToolMicroTESK is an open-source, specification-based test program generation framework for microprocessors developed at ISP RAS. It uses ISA specifications in a dialect of nML, MMU specifications in MMUSL, and Ruby test templates to extract testing situations and dependencies and generate concrete test programs using symbolic execution and constraint solving.
First seen 5/26/2026
Last seen 8/22/2026
Evidence 38 chunks
Wiki v4
WIKI
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
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
50 connectionsMicroTESK is a specification-based tool for constructing test program generators using constraint-based techniques.
MicroTESK uses ADL descriptions to configure the test program generator for target microprocessors.
Cross-level processor verification via endless randomized instruction stream generation with coverage-guided aging ← mentions 90% 4e
The paper mentions MicroTESK as a related tool for test program generation.
MicroTESK uses the SMT-LIB language to formulate constraint satisfaction problems.
MicroTESK is a specification-based tool for constructing test program generators.
MicroTESK uses ADL descriptions to build coverage models for individual instructions.
MicroTESK uses test templates to describe test scenarios and generate test programs.
The test template processor is a component of MicroTESK's testing framework.
MicroTESK is demonstrated with MIPS instruction set architecture examples.
MicroTESK is built around a microprocessor meta-model derived from architecture specifications.
The constraint solver engine is a component of MicroTESK's testing framework.
Test sequence generators are components of MicroTESK's testing framework.
Test data generators are components of MicroTESK's testing framework.
MicroTESK models the instruction set architecture as part of its framework functionality.
MicroTESK supports combinatorial generation as one of its test generation techniques.
MicroTESK uses MMUSL for MMU specifications
MicroTESK implements constraint solving for test data generation
MicroTESK supports template-based generation through its test template processor.
MicroTESK is organized around instruction-level models.
MicroTESK implements symbolic execution for test data generation
MicroTESK uses the MIPS instruction set as an example for specification.
MicroTESK implements constraint-based random generation for test data generation.
Cross-level processor verification via endless randomized instruction stream generation with coverage-guided aging ← compares with 80% 2e
The paper mentions MicroTESK as a related test generator tool.
MicroTESK uses test templates to specify test scenarios.
MicroTESK uses test situations expressed as constraints for test data generation.
MicroTESK uses a design model extracted from formal specifications.
MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors ← introduces 100% 2e
The paper introduces MicroTESK as an ADL-based reconfigurable test program generator.
MicroTESK implements the concept of a reconfigurable test program generator using ADL specifications.
MicroTESK uses SMT solvers for constraint-based test data generation.
MicroTESK formulates and solves constraint satisfaction problems for test data generation.
MicroTESK uses Java Constraint Solver API for SMT-LIB-based constraint solving.
MicroTESK's test template processor supports generation of self-checking tests.
MicroTESK supports random generation as one of its test generation techniques.
MicroTESK builds an instruction set model from ADL specifications.
MicroTESK automatically extracts test knowledge from ADL specifications.
MicroTESK is applied to microprocessor verification
MicroTESK uses buffer-event factorization as a heuristic
MicroTESK uses preparators to generate initialization code
ISP RAS develops the MicroTESK framework
Alexander Kamkin is listed as a manager and project creator of MicroTESK.
Alexander Protsenko is listed as a manager and developer of MicroTESK.
Mikhail Chupilko is listed as a developer of MicroTESK.
The paper cites MicroTESK as a specification-based tool for constructing test program generators.
Sergey Smolov is listed as a developer of MicroTESK.
MicroTESK is a specification-based tool for constructing test program generators, implementing model-based test generation.
The paper mentions MicroTESK as a related test generation framework.
The paper introduces the MicroTESK framework.
MicroTESK uses Sim-nML as its supported ADL for specifying microprocessors.
MicroTESK suggests using Yices as one of the SMT solvers.
MicroTESK suggests using Z3 as one of the SMT solvers.
CITATIONS
9 sources9 citations — click to expand
[1] MicroTESK is an open-license specification-based TPG tool whose version 2.3+ inputs include nML ISA specifications, MMUSL MMU specifications, and Ruby test templates; it extracts situations and dependencies for test generation and template enumeration. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[2] The MicroTESK team describes its goal as creating an open-source, extensible, reconfigurable TPG framework; the MIPS64 MMU work used ISA specifications in nML, MMU specifications in MMUSL, Ruby test templates, symbolic execution, and constraint solving, and identified constraint-solving performance and multicore extension as future work. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[3] The MIPS64 MMU tool based on MicroTESK consists of an architecture-independent generation core and MIPS64 memory-subsystem specifications, and uses MMUSL specifications to extract execution paths and dependencies with symbolic execution and constraint solving for test data. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[4] MicroTESK ISA specifications define data types, constants, registers, access modes, memories, and instructions; MMUSL is used for address types, memory segments, buffers, and load/store control logic. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[5] MMUSL buffer specifications can include associativity, sets, entry format, index and tag functions, and eviction policy; test templates are Ruby subclasses that use specification-defined modes/instructions and TPG constructs such as blocks and situations. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[6] For MMU generation, MicroTESK parses specifications into an ISS interpreter and a labeled DAG, extracts execution paths, derives dependencies over shared buffers, and enumerates symbolic test programs using path/dependency combinations and heuristics. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[7] Symbolic test programs are instantiated with test data such as addresses, buffer entries, and load/evict sequences and then transformed into ISA-specific preparation code. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[8] The MIPS64 MMU case study specified address spaces, TLB entry format, address translation, two-level write-through cache, JTLB/DTLB, L1/L2 caches, selected memory segments, and 18 memory-access instructions; the MMUSL description was approximately 220 lines. Specification-Based Test Program Generation for MIPS64 Memory Management Units
[9] The MicroTESK public project page lists Alexander Kamkin as project creator, Alexander Kamkin and Alexander Protsenko as managers, and Alexander Protsenko, Alexander Kamkin, Mikhail Chupilko, and Sergey Smolov among developers. Overview - MicroTESK - Open-Source Projects