Download catalogue of technologies
MicroTESK: a test program generator
MicroTESK is a reconfigurable and extendable framework for generating test programs for functional verification of microprocessors. MicroTESK allows automatically constructing test program generators based on formal specifications of microprocessor architectures. MicroTESK supports a wide range of architectures including RISC, CISC, VLIW, and DSP. MicroTESK supports online test program generation.
Features and advantages
MicroTESK is a set of technologies for industrial use that includes the basic modeling framework (building microprocessor models based on formal specifications) and the generation framework (building test programs based on test templates). MicroTESK delivers value similar to its global competitors (e.g., Genesys Pro and RAVEN) but outperforms them via increased usability and performance. Also, it is distributed under the open-source Apache 2.0 license. MicroTESK is available at the ISPRAS website: https://forge.ispras.ru/projects/microtesk. The technology is also presented at http://www.microtesk.org.
MicroTESK provides:
- architecture specification in the nML language (registers, memory, addressing modes, instruction logic, text/binary instruction representation);
- additional memory subsystem specifications in the mmuSL language (memory buffer properties (TLB, L1, and L2), address translation logic, read/write operations logic);
- an option to make a transition to formal verification and to automatic toolchain generation for the microprocessor under development (disassembler, emulator, etc.);
- test templates in the Ruby language (so that the templates are human readable and easy to support);
- allows using different generation techniques for instruction sequences and test data simultaneously (random generation, combinatorial generation, constrained-based generation, etc.);
- generation framework scalability (can develop complex test templates at low cost due to reuse).
- supporting architecture specific features for various architectures (RISC, CISC, VLIW, DSP) at the generator development framework level;
- MicroTESK-based test program generators have been developed for RISC-V, ARM, MIPS, and PowerPC architectures;
- multicore architectures are supported.
System requirements
Windows or GNU/Linux-based OS, Java 8.
MicroTESK deployment stories
MicroTESK is developed since 2007. It was used in various Russian and international projects on developing modern industrial microprocessors, including industrial projects on verifying ARMv8, MIPS64, and RISC-V microprocessors.
Workflow

Developer/Participant
Back to the list of technologies of ISP RAS