И.А. Стотланд - к.т.н., доцент, Московский государственный университет информационных технологий, радиотехники и электроники (МИРЭА) E-mail: irastot@mail.ru Н.А. Стариковская - к.т.н., доцент, Московский государственный университет информационных технологий, радиотехники и электроники (МИРЭА) E-mail: starikovskaya@mirea.ru М.А. Кириченко - студент, Московский государственный университет информационных технологий, радиотехники и электроники (МИРЭА) E-mail: kmar.kmar@mail.ru

Описаны подходы к формальной верификации моделей компонентов подсистем коммутации, входящих в состав современных микропроцессоров систем. Отмечено, что подходы основаны на формальной верификации автоматных моделей с помощью метода проверки модели. Дан подробный обзор существующих методов функциональной верификации: имитационного моделирования и формальной верификации. Рассмотрены методы редукции числа состояний и их применимость при верификации моделей подсистем коммутации. Выделены, классифицированы и формализованы свойства, которыми должны обладать подсистемы коммутации микропроцессоров. Приведены результаты практического применения предложенных подходов.

 

1. Bergeron J. Writing testbenches: functional verification of HDL models. Kluwer Academic Publishers. 2003. 478 p.
2. Стотланд И.А., Лагутин А.А. Применение эталонных событийных моделей для автономной верификации модулей микропроцессоров // Вопросы радиоэлектроники. 2014. Т. 4. № 3. С. 17−27.
3. Bentley R.M. Validating the Pentium 4 Microprocessor // Proc. of the Int. Conference on Dependable Systems and Networks. 2001. P. 493−498.
4. Clarke E., Grumberg O., Peled D. Model Checking. MIT Press. 1999. 314 p.
5. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург. 2010. 560 с.
6. Clarke E., Grumberg O., Long O. Model checking and abstraction // ACM Transaction on Programming Languages and Systems. 1994. V. 16. № 5. P. 1512−1542.
7. Drechsler R. Advanced formal verification. Kluwer Academic Publishers. 2014. 628 p.
8. Петроченков М.В., Стотланд И.А. Методика автономной верификации устройств подсистемы памяти многоядерных микропроцессоров // Вопросы радиоэлектроники. 2016. Сер. ЭВТ. № 3. С. 42−47.
9. Камкин А.C., Чупилко М.M. Механизмы поддержки функционального тестирования моделей аппаратуры на разных уровнях абстракции // Труды Института системного программирования РАН. 2011. Т. 20. С. 143−160.
10. Стотланд И.А. Метод динамической верификации модулей системного обмена микропроцессорных вычислительных комплексов // Научно-технич. вестник Поволжья. 2012. № 4. С. 191−196.