MicroTESK: a test program generator

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:

Using formal specification as a source of knowledge about the microprocessor under verification:

• 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 programs generation based on object-oriented test templates:

• 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).

Wide range of supported microprocessor architectures:

• 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.

Quick framework adaptation for the new microprocessor architecture with minimal costs and automatic information extraction for test situations (due to formal specifications);

Convenient language for developing test templates that allows describing complex verification scenarios quickly;

Support for online test program generation for performing post-silicon verification of the target microprocessor. The online generation is performed by an executable generator included into MicroTESK. The generator constructs test sequences using formal specifications, and then modifies the sequences by making functionally equivalent substitutions. It also allows repeated execution of the test sequences on the target microprocessor.

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

Software Engineering