RUS  ENG
Полная версия
ЖУРНАЛЫ // Труды института системного программирования РАН // Архив

Труды ИСП РАН, 2016, том 28, выпуск 4, страницы 41–56 (Mi tisp52)

Эта публикация цитируется в 3 статьях

A model checking-based method of functional test generation for HDL descriptions

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

M. S. Lebedev, S. A. Smolov

Institute for System Programming of the Russian Academy of Sciences

Аннотация: Разработка методов автоматической генерации тестов составляет перспективное направление в области верификации цифровой аппаратуры. На текущий момент большое распространение имеют методы генерации функциональных тестов на основе моделей. В данной работе представлен метод генерации функциональных тестов на основе проверки моделей и результаты его сравнения с существующими решениями. В методе используется автоматическое извлечение моделей из исходного кода HDL-описания аппаратуры. Поддерживаются языки VHDL и Verilog. Метод генерации тестов включает автоматическое построение моделей следующих типов: решающие диаграммы системы охраняемых действий (Guarded Action Decision Diagram,GADD), высокоуровневые решающие диаграммы (High-Level Decision Diagrams, HLDD) и расширенные конечные автоматы (Extended Finite-State Machines, EFSM). HLDD-модель используется в качестве функциональной модели. Модель EFSM используется в качестве модели покрытия. Целью тестирования является покрытие всех переходов расширенного конечного автомата. Выбор такого критерия позволяет получить высокое покрытие исходного кода HDL-описания. Из EFSM-модели извлекаются спецификации, основанные на ограничениях на переходы и состояния. Затем спецификации и функциональная модель автоматически транслируются во входной формат инструмента проверки моделей nuXmv. Инструмент выполняет проверку модели и строит контрпримеры. Контрпримеры транслируются в функциональные тесты, которые могут быть исполнены с помощью HDL-симулятора. Предлагаемый метод был реализован программно в инструменте HDL Rertrascope. Результаты экспериментов показывают, что метод генерирует более короткие тесты, чем методы FATE и RETGA, при обеспечении такого же или лучшего покрытия исходного кода.

Ключевые слова: цифровая аппаратура, функциональная верификация, статический анализ, генерация тестов, охраняемое действие, высокоуровневая решающая диаграмма, расширенный конечный автомат, проверка модели.

Язык публикации: английский

DOI: 10.15514/ISPRAS-2016-28(4)-3



Реферативные базы данных:


© МИАН, 2024