Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK

ARM - это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ - программ на языке ассемблера, создающих разнообразные ситуации (исключения, блокировки конвейера, неверные предсказания переходов, вытеснения данных из кэш-памяти и т.п.). В статье описываются требования, предъявляемые к промышленным генераторам тестовых программ, и представляется генератор для микропроцессоров архитектуры ARMv8, разработанный с использованием инструмента MicroTESK (Microprocessor TEsting and Specification Kit). Генератор поддерживает подмножество команд, характерное для мобильных приложений (около 400 команд) и состоит из двух основных частей: (1) архитектурно независимого ядра и (2) формальной спецификации ARMv8 (точнее, модели, автоматически построенной по формальным спецификациям). При такой организации процесс разработки генератора тестовых программ состоит преимущественно в создании формальных спецификаций, что экономит усилия за счет повторного использования архитектурно независимых компонентов. Архитектура описывается на языках nML и mmuSL: первый язык позволяет описывать регистры микропроцессора, синтаксис и семантику команд; второй - устройство подсистемы памяти (адресные пространства, разного рода буферы и таблицы, алгоритмы трансляции адресов и т.п.). В статье приводятся характеристики разработанного генератора и делается сравнение с существующими аналогами.

микропроцессоры, спецификация системы команд, функциональная верификация, генерация тестовых программ, ARM, nML, MicroTESK

1. Сайт компании ARM. 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. Камкин А.С. Генерация тестовых программ для микропроцессоров. Труды ИСП РАН, том 14, часть 2, 2008. с. 23-64.

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. Труды ИСП РАН, vol. 28, issue 4, 2016. pp. 81-102. DOI: 10.15514/ISPRAS-2016-28(4)-5