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


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

М.М. Чупилко (ИСП РАН, Москва, Россия)
А.С. Камкин (ИСП РАН, Москва, Россия; МГУ, Москва, Россия; МФТИ, Долгопрудный, Россия)
М.С. Лебедев (ИСП РАН, Москва, Россия)
С.А. Смолов (ИСП РАН, Москва, Россия)

Аннотация

Тестирование аппаратуры — это процесс, нацеленный на обнаружение неисправностей, внесенных в интегральные схемы в процессе производства. Для оценки качества таких тестов используют две основные метрики: способность обнаруживать ошибки (покрытие ошибок) и время тестирования (длина теста). Известно множество методов генерации тестов, однако масштабируемого решения, применимого к сложной цифровой аппаратуре, нет до сих пор. В данной статье анализируется возможность использования функциональных тестов, построенных по высокоуровневым моделям (прежде всего, моделям уровня регистровых передач), для низкоуровневого производственного тестирования. Рассматривается конкретный метод генерации тестов, использующий технику проверки моделей (model checking). Входной информацией выступает HDL-описание. Метод состоит из двух ключевых шагов: построение модели системы и построение модели покрытия. Указанные модели автоматически извлекаются из HDL-описания. Модель системы представлена в виде высокоуровневых решающих диаграмм. Модель покрытия — это множество LTL-формул, определяющих условия достижимости переходов расширенного конечного автомата, описывающего систему. Построенные модели транслируются во входной формат инструмента проверки моделей (model checker), который для каждой формулы модели покрытия генерирует контрпример — вычисление, нарушающее эту формулу, то есть приводящее к срабатыванию соответствующего перехода автомата. Изначально рассматриваемый метод предназначался для покрытия всех путей исполнения HDL-описания и обнаружения недостижимого кода. Экспериментальное сравнение метода с существующими аналогами показало, что он строит более короткие тесты, однако эти тесты достигают меньшего уровня покрытия константных неисправностей, чем тесты, построенные с помощью специальных средств. В статье предлагается модификация метода для преодоления указанного недостатка.

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

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

Издание

Труды Института системного программирования РАН, том 29, вып. 4, 2017, стр. 247-256.

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

DOI: 10.15514/ISPRAS-2017-29(4)-16

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