Институт системного программирования им. В.П. Иванникова РАН


Динамическая верификация цифровой аппаратуры на основе формальных спецификаций

M. M. Чупилко. Начало семинара - 17 апреля 2012 г.

Сложные системы, к которым относится цифровая аппаратура, проектируются от общего к частному: сначала создается обобщенное представление системы, может быть создана ее модель, затем происходит декомпозиция системы на составные части, определяется порядок их взаимодействия. Подобным же образом может проводиться и верификация, причем определенная технология построения тестовых систем может помочь достичь большого уровня повторного использования их обобщенных частей, что существенно экономит ресурсы на их разработку. Также следует отметить, что для аппаратуры характерен высокий уровень параллелизма, что приводит к конкурентному доступу к общим ресурсам и «комбинаторному взрыву» числа состояний.

В результате проведенной работы был предложен метод верификации моделей цифровой аппаратуры, описывающий архитектуру тестовых систем, масштабируемую на разные уровни абстракции и построенную на основе формальных спецификаций особого вида, учитывающих особенности работы цифровой аппаратуры и поддерживающих композицию. На основе предложенного метода была разработана программная библиотека классов на языке C++ для инструмента C++TESK, которая была использована для верификации ряда модулей микропроцессоров, разрабатываемых в НИИ системных исследований РАН и ЗАО «Московский центр спарк-технологий». Разработанные тестовые системы позволили выявить ряд критических ошибок, обнаружение которых при использовании других методов верификации принципиально сложно. Тестовые системы, как правило, использовали части системных симуляторов микропроцессоров, тем самым увеличивая степень их повторного использования и скорость проведения верификации.

С предварительной презентацией доклада можно ознакомиться здесь.

С презентацией доклада можно ознакомиться здесь.

Семинар группы

Технологии программирования

Перейти к списку семинаров ИСП РАН