MicroTESK: Specification-Based Tool for Constructing Test Program Generators
The paper presents MicroTESK, a tool that automates construction of test program generators for microprocessors. A constructed generator consists of the core that implements architecture-independent generation methods and the model that holds information required to generate tests for the corresponding architecture. The tool extracts this information from formal specifications of the instruction set architecture. The extracted information is used in multiple ways: (1) to get the assembly format of the instructions; (2) to build the coverage model of the instruction set architecture; (3) to construct the instruction set simulator used as a reference model. Test programs are created on the basis of test templates provided by users. Flexible architecture of the tool facilitates integration of new test generation engines. MicroTESK has been applied to the ARMv8, MIPS64, PowerPC, RISC-V, and x86 architectures.
KeywordsMicroprocessors Functional verification Test program generation Instruction set architectures Formal specifications
Unable to display preview. Download preview PDF.
- 2.RAVEN Test Program Generator. http://www.slideshare.net/DVClub/introducing-obsidian-software-andravengcs-for-powerpc
- 3.MicroTESK Page. http://forge.ispras.ru/projects/microtesk
- 4.Freericks, M.: The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department (1993)Google Scholar
- 5.Tatarnikov, A.: Language for describing templates for test program generation for microprocessors. In: Proceedings of ISP RAS, vol. 28, no. 4, pp. 81–102 (2016)Google Scholar
- 6.Chupilko, M., Kamkin, A., Kotsynyak, A., Protsenko, A., Smolov, S., Tatarnikov, A.: Specification-based test program generation for ARM VMSAv8-64 memory management units. In: Workshop on Microprocessor Test and Verification, pp. 1–6 (2015)Google Scholar