MicroTESK: Specification-Based Tool for Constructing Test Program Generators

  • Mikhail Chupilko
  • Alexander Kamkin
  • Artem Kotsynyak
  • Andrei TatarnikovEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10629)


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.


Microprocessors Functional verification Test program generation Instruction set architectures Formal specifications 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Adir, A., Almog, E., Fournier, L., Marcus, E., Rimon, M., Vinov, M., Ziv, A.: Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. Design & Test of Computers 21(2), 84–93 (2004)CrossRefGoogle Scholar
  2. 2.
  3. 3.
  4. 4.
    Freericks, M.: The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department (1993)Google Scholar
  5. 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. 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

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Mikhail Chupilko
    • 1
  • Alexander Kamkin
    • 1
    • 2
    • 3
  • Artem Kotsynyak
    • 1
  • Andrei Tatarnikov
    • 1
    Email author
  1. 1.Ivannikov Institute for System Programming of the Russian Academy of SciencesMoscowRussia
  2. 2.Lomonosov Moscow State UniversityMoscowRussia
  3. 3.Moscow Institute of Physics and TechnologyMoscowRussia

Personalised recommendations