Автономная верификация IOMMU с поддержкой виртуализации
https://doi.org/10.15514/ISPRAS-2019-31(3)-7
Аннотация
В данной статье представлен подход к автономной верификации блока управления памятью ввода / вывода с поддержкой виртуализации. Мы представляем базовую архитектуру тестовой системы. Рассматриваются основные проблемы, возникающие при верификации IOMMU с поддержкой виртуализации. Одной из ключевых проблем стало формирование страниц таблицы трансляции. Количество таблиц трансляции зависит от режима работы IOMMU и типа трансляции. В качестве решения этой проблемы предложен подход к динамической генерации таблиц трансляции. Представлен алгоритм формирования страниц таблиц трансляции в генераторе. Решается проблема проверки трансляции виртуального адреса в физический с использованием двухуровневых таблиц трансляций. Рассмотрены особенности реализации эталонной модели. Описаны эталонная модель и тестовая система, которые использовались для верификации микропроцессора IOMMU с архитектурой 6-го поколения «Эльбрус». Представлены методы связи между тестовой системой и моделью IOMMU. Рассматриваются результаты проверки IOMMU.
Ключевые слова
Об авторах
Антон Алексеевич Петрыкин
АО "МЦСТ"
Россия
Россия
Ирина Аркадьевна Стотланд
АО "МЦСТ"
Россия
Россия
Алексей Николаевич Мешков
АО "МЦСТ";
ПАО «ИНЭУМ им. И.С.Брука»
Россия
Россия
Список литературы
1. Intel Virtualization Technology for Directed I/O Architecture Specification. Intel, 2018.
2. AMD I/O Virtualization Technology (IOMMU) Specification. AMD, 2016.
3. Lebedev D.A., Stotland I.A. Construction of validation modules based on reference functional models in a standalone verification of communication subsystem. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 3, 2018, pp. 183-194. DOI: 10.15514/ISPRAS-2016-28(3)-10.
4. Alkassar E., Cohen E., Kovalev M., Paul W.J. (2012) Verification of TLB Virtualization Implemented in C. Lecture Notes in Computer Science, vol 7152, pp 209-224.
5. Alkassar, E., Cohen, E., Hillebrand, M., Kovalev, M., Paul, W. Verifying shadow page table algorithms. In Formal Methods in Computer Aided Design (FMCAD), 2010. pp. 267-270.
6. Kamkin A., Kotsynyak A. Specification-Based Test Program Generation for MIPS64 Memory Management Units. Trudy ISP RAN/Proc, ISP RAS vol. 28, issue 4, 2016. pp. 99-114. DOI: 10.15514/ISPRAS-2016-28(4)-6.
7. IEEE Standard for SystemVerilog — Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2012.
8. 1800.2-2017 - IEEE Standard for Universal Verification Methodology Language Reference Manual.
Рецензия
Для цитирования:
Петрыкин А.А., Стотланд И.А., Мешков А.Н. Автономная верификация IOMMU с поддержкой виртуализации. Труды Института системного программирования РАН. 2019;31(3):77-84. https://doi.org/10.15514/ISPRAS-2019-31(3)-7
For citation:
Petrykin A.A., Stotland I.A., Meshkov A.N. Standalone verification of IOMMU with virtualization supporting. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(3):77-84. https://doi.org/10.15514/ISPRAS-2019-31(3)-7
Послать статью по эл. почте 