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 techniques.
The purpose of MTV is to bring researchers and practitioners from the fields of verification, security and test together to exchange innovative ideas and to develop new methodologies to solve the difficult challenges facing us today in various processor and SOC design environments. In the past few years, some work has been done on exploiting techniques from test to solve problems in security and verification and vice versa. This is the 18th edition of the MTV Workshop, a testament to its success in providing an ideal environment for cross- examination of test, security and verification experiences and innovative solutions.
More details can be found in the slides and the following paper: