Preview

Вопросы радиоэлектроники

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

МЕТОДИКА АВТОНОМНОЙ ВЕРИФИКАЦИИ УСТРОЙСТВ ПОДСИСТЕМЫ ПАМЯТИ МНОГОЯДЕРНЫХ МИКРОПРОЦЕССОРОВ

Полный текст:

Аннотация

Приведена оценка классических подходов к автономной верификации устройств подсистемы памяти. Предложены методы проверки корректности, построенные на основе учета «подсказок» от реализации и применении утверждений. Описан подход к автономной верификации событийно-недетерменированных устройств, вводящий динамическое уточнение вариантов поведения модели на базе реакций от реализации. Приводится опыт применения рассмотренных методов при верификации устройств подсистемы памяти восьмиядерных микропроцессоров с архитектурой «Эльбрус».

Об авторах

М. В. Петроченков
АО «МЦСТ»
Россия

научный сотрудник, 

117105, Москва, ул. Нагатинская, д. 1, стр.23, тел. (499) 135-44-61.



И. А. Стотланд
АО «МЦСТ»
Россия

к. т.н., начальник сектора,

117105, Москва, ул. Нагатинская, д. 1, стр. 23, тел. (499) 135-44-71.



Список литературы

1. Revision Guide for AMD Family 15h Models 30h-3Fh Processors. — [Электронный ресурс]. — Режим доступа: http://www.developer.amd.com/resources/documentation-articles/developer-guides-manuals (дата обращения 20.12.2015).

2. Intel® Atom™ Processor C2000 Product Family. Specification Update. December 2015. — [Электронный ресурс]. — Режим доступа: http://www.intel.com/content/www/us/en/processors/atom/atop-c2000-family-spec-update.html (дата обращения 20.12.2015).

3. Стотланд, И.А., Куцевол, В.Н., Мешков, А. Н. Проблемы функциональной верификации кэш-памяти второго уровня микропроцессоровс архитектурой «Эльбрус» // Вопросы радиоэлектроники.— 2015.— Сер. ЭВТ.— Вып. 1.— С. 76—84.

4. TLM-2.0.1. TLM Transaction-Level Modeling Library. — [Электронный ресурс]. — Режим доступа: http://www.accellera.org/downloads/standards/systemc (дата обращения 20.12.2015).

5. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. — СПб.: БХВ-Петербург, 2010. — 560 с.

6. Стотланд, И.А., Лагутин, А. А. Применение эталонных событийных моделей для автономной верификации модулей микропроцессоров // Вопросы радиоэлектроники. — 2014. — Сер. ЭВТ. — Вып. 3. — С. 17—27.

7. Камкин, А.С., Петроченков, М. В. Метод построения тестового оракула для подсистемы памяти микропроцессора на основе недетерминированной функциональной модели // Вопросы радиоэлектроники. — 2015. — Сер. ЭВТ. — Вып.1. — С. 84—95.

8. Кожин, А.С., Кожин, Е.С., Костенко, В. О. Кэш третьего уровня и поддержка когерентности микропроцессора «Эльбрус-4С+» // Вопросы радиоэлектроники. — 2013. — Сер. ЭВТ. — Вып.3. — С.26—38.


Для цитирования:


Петроченков М.В., Стотланд И.А. МЕТОДИКА АВТОНОМНОЙ ВЕРИФИКАЦИИ УСТРОЙСТВ ПОДСИСТЕМЫ ПАМЯТИ МНОГОЯДЕРНЫХ МИКРОПРОЦЕССОРОВ. Вопросы радиоэлектроники. 2016;(3):42-47.

For citation:


Petrochenkov M., Stotland I. METHODS OF STANDALONE VERIFICATION OF MULTI-CORE MICROPROCESSOR MEMORY SUBSYSTEM UNITS. Issues of radio electronics. 2016;(3):42-47. (In Russ.)

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


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


ISSN 2218-5453 (Print)
ISSN 2686-7680 (Online)