Сборники трудов ИСП РАН


Подход к генерации тестов, нацеленных на покрытие кода HDL-описаний аппаратуры, на основе расширенных конечных автоматов

И.В. Мельниченко (ИНЭУМ, Москва), А.С. Камкин (ИСП РАН, Москва), С.А. Смолов (ИСП РАН, Москва)

Аннотация

Генерация тестов по моделям широко используется для функциональной верификации аппаратуры. Расширенные конечные автоматы (extended finite state machines, EFSM) — удобный формализм для моделирования цифровых устройств. В отличие от обычных конечных автоматов, в EFSM-моделях управляющие сигналы и данные разделены, что позволяет описывать системы в более компактной форме, уменьшая в некотором смысле риск комбинаторного взрыва при верификации. Однако обход графа состояний EFSM-модели является нетривиальной задачей из-за наличия условий на выполнимость переходов. В данной статье представлен метод генерации тестов по EFSM-моделям и проведено его сравнение с другими подходами. Предлагаемый метод сочетает случайный обход графа состояний автомата и направленный поиск реализуемых путей. Первая из указанных фаз направлена на покрытие «простых» переходов, вторая — «сложных». Под сложностью переходов здесь понимается наличие зависимостей охранных условий переходов от внутренних переменных. При направленном поиске используется информация о зависимостях по данным и управлению между переходами автомата и задействуется символическое исполнение. Было выполнено сравнение предлагаемого метода с существующими аналогами путем сопоставления параметров тестов, сгенерированных для заданного набора описаний модулей цифровой аппаратуры. Во всех случаях в качестве входных данных использовались EFSM-модели, автоматически извлеченные из кода. Полученные данные показывают, что в сравнении с другими подходами метод обеспечивает лучшие показатели покрытия исходного кода более короткими тестами. В будущем планируется реализовать ряд оптимизаций, направленных на применение метода к промышленным HDL-описаниям.

Ключевые слова

проектирование аппаратуры; язык описания аппаратуры; имитационная верификация; генерация тестов; моделирование; расширенный конечный автомат; обход графа; случайный обход; поиск с возвратами; символическое исполнение; разрешение ограничений

Издание

Труды Института системного программирования РАН, том 27, вып. 3, 2015, стр. 161-182.

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

DOI: 10.15514/ISPRAS-2015-27(3)-12

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома