Category: New Features

Andrei Tatarnikov (MicroTESK Core Team Lead) defended his PhD thesis on MicroTESK at Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISP RAS). The title is “Automated Construction of Test Program Generators for Microprocessors Based on Formal Specifications”. Congratulations!

The recent MicroTESK build (2.4.34) supports two nML extensions that ease developing and maintaining ISA specifications: templates and revisions. Templates allow defining families of operations whose operands differ only in their data types. To describe an operation in a generic way, the following constructs have been introduced: type_of, size_of, and is_type. Here is an example. op cmd_B(op1: BYTE, ...) ... op cmd_D(op1: DWORD, ...) action = { ... } Revisions allows enabling/disabling ISA elements (registers, operations, etc.) depending on the current ISA version. In the example below, the cmd_v2 operation is enabled only when the CPU_V2 revision is turned on. @rev(CPU_V2) op cmd_v2(rd: REG, rn: REG) To define different versions of the same ISA element, the @rev construct can be applied to the element attributes (syntax, action, etc.). Here comes an example.…

MicroTESK was presented at the A.P. Ershov Informatics Conference (the PSI Conference Series, 11th edition) held in Moscow, Russia on June 27-29, 2017. We made the following presentation: A. Kamkin, A. Tatarnikov. MicroTESK: A Tool for Constrained-Random Test Program Generation for Microprocessors. PSI is the premier international forum in Russia for research and applications in Computer Science (CS) and Software Engineering (SE). PSI is held regularly since 1991. The conference brings together academic and industrial researchers, developers and users to discuss the most recent topics in the field. PSI provides an ideal venue for setting up research collaborations between the growing Russian CS/SE researcher community and its international counterparts, as well as between established scientists and younger researchers.  

As you may know, the GNU Assembler (GAS) as well as the ELF and COFF object file formats supports so-called sections. Section is a contiguous piece of code located at a specified memory address. Besides the starting address, each section is described with a number of attributes such as name, size, etc. The recent MicroTESK build (2.4.27) allows using sections in test templates. It supports two predefined sections: .data (constants and variables) and .text (executable code). Also, there is a possibility to define custom sections. Syntactically, sections are blocks that wrap data or code declarations. section_data(...) { # .data word 0, 1, 2 ... } section_text(...) { # .text sequence { add t0, t1, t2 ... }.run } section(:name => 'name', ...) { # .section name ... } Each section…

The recent MicroTESK build (2.4.17) contains the revisited x86 (8086) demo with the ISA specification and test templates illustrating the basic facilities of the tool. The build can be downloaded from the link below: http://forge.ispras.ru/…/microtesk-2.4.17-beta-170407.tar.gz Here is a brief explanation how to get started with the demo: http://forge.ispras.ru/…/micr…/wiki/Getting_Started_with_x86  

We are happy to announce that we made the MicroTESK for MIPS64 project open source. The package consisting of the MicroTESK core, the MIPS64 (Revision 6) specifications, and the basic test templates is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose: to distribute it, to modify it, and to distribute modified versions of the software. Feel free to contact us if you have any questions. MIPS is a trademark of Imagination Technologies LTD.

We started a new version of MicroTESK, namely 2.4. Our goal is to support verification of microprocessors with multiple processing elements (PE). The main idea is to maintain several instances of instruction set simulator (ISS) resources during test program generation. Each instance is initialized according to the rules defined in the ‘instantiate’ operation. op instantiate(id: WORD) action = { Reg1 = Expr1(id); ... RegN = ExprN(id); } The number of instances used by the test program generator is set by the ‘instance-number’ option (by default, it is equal to 1). The MicroTESK distribution package can be downloaded from http://forge.ispras.ru/projects/microtesk/files.

MicroTESK will be presented at the 10th Spring/Summer Young Researchers' Colloquim on Software Engineering (SYRCoSE). The event will take place on May 30 - June 1, 2016 in the Recreation Center of Moscow State University (Krasnovidovo, Mozhaysk Region). We will make the following presentations: A. Kamkin, A. Kotsynyak. Specification-Based Test Program Generation for MIPS64 Memory Management Units. A. Tatarnikov. Language for Describing Templates for Test Program Generation for Microprocessors. SYRCoSE is an annual colloquium on software engineering targeted at young researchers (students, postgraduates, young PhDs, etc.). The main goal of the colloquium is to help young specialists to meet each other, to get more information on work of their colleagues, to exchange their experience, and to practice in presenting their results at international conferences and workshops.  

MicroTESK for ARMv8 will be presented at the 16th annual workshop on Microprocessor Test and Verification (MTV) to be held in Austin, TX on December 3-4, 2015. The presentation describes a tool for automatically generating test programs for ARM VMSAv8-64 memory management units. It consists of two parts: an architecture-independent test program generation core (MicroTESK) and VMSAv8-64 specifications. The specifications comprise descriptions of the memory access instructions, loads and stores, and definition of the memory management mechanisms such as translation lookaside buffers, page tables, and cache units. The tool analyzes the specifications and extracts the execution paths and inter-path dependencies. The extracted information is used to systematically enumerate test programs for a user-defined test template. Test data for a particular program are generated by using symbolic execution and constraint solving…

MicroTESK's floating-point functionality is based on Java SoftFloat, which is a Java implementation of the Berkeley SoftFloat library, a free, high-quality software implementation of binary floating-point that conforms to the IEEE Standard for Floating-Point Arithmetic. As the original version, Java SoftFloat fully implements four floating-point formats: 32-bit single-precision, 64-bit double-precision, 80-bit double-extended-precision, and 128-bit quadruple-precision. Java SoftFloat is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer. The current implementation (v1.0) corresponds to SoftFloat Release 2b (2002 May 27).