Year: 2015

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

The released version of MicroTESK (v2.3) supports test program generation for MMU. The approach is based on formal specifications of memory access instructions (loads and stores) and buffers (TLB, L1/L2, etc.). Test programs are generated by enumerating all feasible situations (instruction execution paths) and dependencies (sets of inter-instruction conflicts) for a given memory access template. It is important that situations and dependencies are automatically extracted from specifications. New version can be downloaded from the page http://forge.ispras.ru/projects/microtesk/files.