MicroTESK-Based Test Program Generator for the ARMv8 Architecture
Autor: | A. S. Kamkin, A. M. Kotsynyak, A. S. Protsenko, A. D. Tatarnikov, M. M. Chupilko |
---|---|
Rok vydání: | 2016 |
Předmět: |
nml
Generator (computer programming) Functional verification Assembly language Computer science Semantics (computer science) Programming language функциональная верификация Pipeline (computing) микропроцессоры computer.software_genre lcsh:QA75.5-76.95 генерация тестовых программ Instruction set microtesk Computer architecture Formal specification arm Virtual memory спецификация системы команд General Earth and Planetary Sciences lcsh:Electronic computers. Computer science computer General Environmental Science computer.programming_language |
Zdroj: | Труды Института системного программирования РАН, Vol 28, Iss 6, Pp 87-102 (2018) |
ISSN: | 2220-6426 2079-8156 |
DOI: | 10.15514/ispras-2016-28(6)-6 |
Popis: | 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. |
Databáze: | OpenAIRE |
Externí odkaz: |