MicroTESK

Tool

MicroTESK, short for Microprocessor TEsting and Specification Kit, is a framework for generating assembly-language test programs for functional verification of microprocessors. It uses formal specifications to describe the microprocessor under verification, expresses generation tasks in a Ruby-based language, and has been applied in industrial verification projects for ARMv8 and MIPS64 microprocessors.

First seen 5/26/2026

Last seen 7/4/2026

Evidence 28 chunks

Wiki v3

WIKI

MicroTESK

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.

Purpose and generation model

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

50 connections

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.

Architecture Description Language uses → 100% 4e

MicroTESK uses ADL descriptions to configure the test program generator for target microprocessors.

Constraint-based Test Generation implements → 90% 4e

MicroTESK is a specification-based tool for constructing test program generators using constraint-based techniques.

test templates uses → 100% 3e

MicroTESK uses test templates to describe test scenarios and generate test programs.

Coverage Model uses → 100% 3e

MicroTESK uses ADL descriptions to build coverage models for individual instructions.

SMT-LIB uses → 100% 3e

MicroTESK uses the SMT-LIB language to formulate constraint satisfaction problems.

Design Model uses → 100% 2e

MicroTESK uses a design model extracted from formal specifications.

SMT Solver uses → 100% 2e

MicroTESK uses SMT solvers for constraint-based test data generation.

Constraint Satisfaction Problem uses → 100% 2e

MicroTESK formulates and solves constraint satisfaction problems 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.

Java Constraint Solver API uses → 100% 2e

MicroTESK uses Java Constraint Solver API for SMT-LIB-based constraint solving.

Self-Checking Test implements → 100% 2e

MicroTESK's test template processor supports generation of self-checking tests.

Instruction Set Model uses → 100% 2e

MicroTESK builds an instruction set model from ADL specifications.

Test Knowledge uses → 100% 2e

MicroTESK automatically extracts test knowledge from ADL specifications.

test program generation implements → 100% 2e

MicroTESK implements test program generation techniques.

MIPS Instruction Set Architecture uses → 90% 2e

MicroTESK is demonstrated with MIPS instruction set architecture examples.

Microprocessor Architecture Model uses → 100% 2e

MicroTESK is built around a microprocessor meta-model derived from architecture specifications.

Test Template Processor ← part of 100% 2e

The test template processor is a component of MicroTESK's testing framework.

Constraint Solver Engine ← part of 100% 2e

The constraint solver engine is a component of MicroTESK's testing framework.

Test Sequence Generator ← part of 100% 2e

Test sequence generators are components of MicroTESK's testing framework.

Test Data Generator ← part of 100% 2e

Test data generators are components of MicroTESK's testing framework.

Instruction Set Architecture uses → 100% 2e

MicroTESK models the instruction set architecture as part of its framework functionality.

Random Generation implements → 100% 2e

MicroTESK supports random generation as one of its test generation techniques.

Combinatorial Generation implements → 100% 2e

MicroTESK supports combinatorial generation as one of its test generation techniques.

Template-Based Generation implements → 95% 2e

MicroTESK supports template-based generation through its test template processor.

Constraint-Based Random Generation implements → 100% 2e

MicroTESK implements constraint-based random generation for test data generation.

MIPS Instruction Set uses → 90% 2e

MicroTESK uses the MIPS instruction set as an example for specification.

Instruction-Level Model uses → 100% 2e

MicroTESK is organized around instruction-level models.

Test Template uses → 100% 2e

MicroTESK uses test templates to specify test scenarios.

Test Situation uses → 100% 2e

MicroTESK uses test situations expressed as constraints for test data generation.

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.

Reconfigurable Test Program Generator implements → 100% 2e

MicroTESK implements the concept of a reconfigurable test program generator using ADL specifications.

Pipeline Control Unit uses → 85% 1e

MicroTESK models and verifies the pipeline control unit as a microprocessor subsystem.

Model-Based Test Generation implements → 90% 1e

MicroTESK is a specification-based tool for constructing test program generators, implementing model-based test generation.

MicroTESK: An Extendable Framework for Test Program Generation ← introduces 100% 1e

The paper introduces the MicroTESK framework.

Sim-nML uses → 100% 1e

MicroTESK uses Sim-nML as its supported ADL for specifying microprocessors.

Yices uses → 95% 1e

MicroTESK suggests using Yices as one of the SMT solvers.

Z3 uses → 95% 1e

MicroTESK suggests using Z3 as one of the SMT solvers.

test oracle uses → 95% 1e

MicroTESK injects test oracle code to verify microprocessor state.

Memory Management uses → 100% 1e

MicroTESK supports memory management as a standard extension.

Pipeline Model uses → 100% 1e

MicroTESK supports pipeline modeling as a standard extension.

Test Program Composition uses → 90% 1e

MicroTESK supports test program composition as a feature.

Mutation-based Compliance Testing for RISC-V ← mentions 85% 1e

The paper references MicroTESK as a specification-based test program generator.

Assembly-level test program generation implements → 95% 1e

MicroTESK is described as a framework that generates assembly-language test programs, directly implementing assembly-level test generation.

Formal specification-driven test generation implements → 90% 1e

The tool uses formal specifications and derives test situations from them, matching the formal specification-driven test generation technique.

ARMv8 targets ISA → 90% 1e

The tool has been applied to verify ARMv8 microprocessors, indicating it targets the ARMv8 ISA.

MIPS64 targets ISA → 90% 1e

The tool has been applied to verify MIPS64 microprocessors, indicating it targets the MIPS64 ISA.

nML uses → 100% 1e

MicroTESK supports nML as one of its supported ADLs.

Sim-nML uses → 100% 1e

MicroTESK supports Sim-nML as one of its supported ADLs.

Configuration Files uses → 100% 1e

MicroTESK uses configuration files for microprocessor subsystems not easily described in ADLs.

LINKED ENTITIES

4 links

Assembly-level test program generation IMPLEMENTS Extracted graph relationship

Formal specification-driven test generation IMPLEMENTS Extracted graph relationship

ARMv8 TARGETS_ISA Extracted graph relationship

MIPS64 TARGETS_ISA Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[1] MicroTESK stands for Microprocessor TEsting and Specification Kit and is a framework for generating assembly-language test programs for functional verification of microprocessors. MicroTESK: a test program generator

[2] MicroTESK uses formal specifications as a source of knowledge about the configuration of the microprocessor under verification. MicroTESK: a test program generator

[3] MicroTESK generation tasks are described in a special Ruby-based language that expresses verification goals as test situations derived from formal specifications, simplifying configuration and improving test coverage. MicroTESK: a test program generator

[4] A 2013 description presents MicroTESK as an extendable test-program-generation framework combining microprocessor modeling and testing techniques, with a central part built around instruction-level models and random/combinatorial test program generators. MicroTESK: An Extendable Framework for

[5] MicroTESK's constraint solver engine is a framework component that constructs test data by solving constraints from test situations and encapsulates universal and custom solvers behind a generic interface. MicroTESK: An Extendable Framework for

[6] MicroTESK uses the Java Constraint Solver API as a generic interface to SMT-LIB-based constraint solvers, with support for Java-side constraint creation, SMT-LIB mapping, solver launch, and result transfer. MicroTESK: An Extendable Framework for

[7] MicroTESK can use external SMT solvers such as Yices and Z3 for universal solving, while custom solvers or generators can be supplied for hard-to-express situations such as floating-point arithmetic and memory management. MicroTESK: An Extendable Framework for

[8] MicroTESK has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors. MicroTESK: a test program generator