An extended finite state machine-based approach to code coverage-directed test generation for hardware designs

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