Preview

Труды Института системного программирования РАН

Расширенный поиск

Автономная верификация 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

Просмотров: 133


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)