MicroTESK-Based Test Program Generator for the ARMv8 Architecture

ARM is a family of microprocessor instruction set architectures developed in a company with the same name. The newest architecture of this family, ARMv8, contains a large number of instructions of various types and is notable for its complex organization of virtual memory, which includes hardware support for multilevel address translation and virtualization. All of this makes functional verification of microprocessors with this architecture an extremely difficult technical task. An integral part of microprocessor verification is generation of test programs, i.e. programs in the assembly language, which cause various situations (exceptions, pipeline stalls, branch mispredictions, data evictions in caches, etc.). The article describes the requirements for industrial test program generators and presents a generator for microprocessors with the ARMv8 architecture, which has been developed with the help of MicroTESK (Microprocessor TEsting and Specification Kit). The generator supports an instruction subset typical for mobile applications (about 400 instructions) and consists of two main parts: (1) an architecture-independent core and (2) formal specifications of ARMv8 or, more precisely, a model automatically constructed on the basis of the formal specifications. With such a structure, the process of test program generator development consists mainly in creation of formal specifications, which saves efforts by reusing architecture-independent components. An architecture is described using the nML and mmuSL languages. The first one allows describing the microprocessor registers and syntax and semantics of the instructions. The second one is used to specify the memory subsystem organization (address spaces, various buffers and tables, address translation algorithms, etc.) The article describes characteristics of the developed generator and gives a comparison with the existing analogs.

microprocessors, instruction set specification, functional verification, test program generation, ARM, nML, MicroTESK

1. ARM site. http://www.arm.com.

2. Mallya H. The Backstory of How ARM Reached a Milestone of 86 Billion Chips in 25 Years. July 19, 2016 (https://yourstory.com/2016/07/arm-holdings-story/).

3. Morgan T.P. ARM Holdings Eager for PC and Server Expansion. Record 2010, Looking for Intel Killer 2020. February 1, 2011 (http://www.theregister.co.uk/2011/02/01/arm_holdings_q4_2010_numbers/).

4. Sims G. Custom Cores versus ARM Cores, What Is It All About? January 7, 2016 (http://www.androidauthority.com/arm-cortex-core-custom-core-kryo-explained-664777/).

5. ARM Architecture Reference Manual. ARM DDI 0487A.f, ARM Corporation, 2015. 5886 p.

6. Kamkin A. Test Program Generation for Microprocessors. Trudy ISP RAN / Proc. ISP RAS, volume 14, part 2, 2008, pp. 23-64 (in Russian).

7. 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), 2004. pp. 84-93. DOI: 10.1109/MDT.2004.1277900.

8. Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Spring/Summer Young Researchers' Colloquium on Software Engineering, 2012. pp. 64-69. DOI: 10.15514/SYRCOSE-2012-6-8.

9. Freericks M. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993.

10. Chupilko M., Kamkin A., Kotsynyak A., Protsenko A., Smolov S., Tatarnikov A. Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units. Workshop on Microprocessor Test and Verification, 2015. pp. 1-6. DOI: 10.1109/MTV.2015.13.

11. Hrishikesh M.S., Rajagopalan M., Sriram S., Mantri R. System Validation at ARM — Enabling our Partners to Build Better Systems. White Paper. April 2016 (http://www.arm.com/files/pdf/System_Validation_at_ARM_Enabling_our_partners_to_build_better_systems.pdf).

12. Venkatesan D., Nagarajan P. A Case Study of Multiprocessor Bugs Found Using RIS Generators and Memory Usage Techniques. Workshop on Microprocessor Test and Verification, 2014. pp. 4-9. DOI: 10.1109/MTV.2014.28.

13. Hudson J., Kurucheti G. A Configurable Random Instruction Sequence (RIS) Tool for Memory Coherence in Multi-processor Systems. Workshop on Microprocessor Test and Verification, 2014. pp. 98-101. DOI: 10.1109/MTV.2014.26.

14. RAVEN test program generator (http://www.slideshare.net/DVClub/introducing-obsidian-software-andravengcs-for-powerpc).

15. Adir A., Fournier L., Katz Y., Koyfman A. DeepTrans – Extending the Model-based Approach to Functional Verification of Address Translation Mechanisms. High-Level Design Validation and Test Workshop, 2006. pp. 102-110.

16. Tatarnikov A.D. Language for Describing Templates for Test Program Generation for Microprocessors. Trudy ISP RAN / Proc. ISP RAS, volume 28, part 4, 2016. pp. 81-102. DOI: 10.15514/ISPRAS-2016-28(4)-5