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

Разработка методов автоматической генерации тестов составляет перспективное направление в области верификации цифровой аппаратуры. На текущий момент большое распространение имеют методы генерации функциональных тестов на основе моделей. В данной работе представлен метод генерации функциональных тестов на основе проверки моделей и результаты его сравнения с существующими решениями. В методе используется автоматическое извлечение моделей из исходного кода 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, при обеспечении такого же или лучшего покрытия исходного кода.