sumn_mcy

Введение

Тестирование стенда с использованием мутаций с помощью MCY (Mutation Coverage with Yosys)

В этом проекте представлен пример тестирования отладочного стенда для модуля sum_n.

Описание формального тестирования модуля sum_n вы можете посмотреть в статье К формальной проверке на fpga-systems.ru. Проект формального тестирования можно взять от сюда.

Как использовать

Клонируйте репу

Сгенерируйте проект. Выполните

Получите помощь

Возможно вам необходимо будет установить переменную SCRIPTS. Укажите свой путь.

Выполните тестирование созданного проекта

Вы можете делать это по частям: Убедитесь в том, что testbench работает

Если у вас установлен gtkwave, то вы сразу увидете эпюры.

Чтобы очистить артефакты testbench выполните

Проверка тестовой среды

Выполните проверку работоспособности тестовой среды

Выполните проверку работоспособности теста на эквивалентность

либо вместе

Получите

Настройка testbench

По умолчанию testbench создает наборы данных генерируя их случайным образом. Это создаст довольно много мутаций. Для отладки вы можете ускорить работу заменив наборы данных в testbench на пред установленные вручную. Тогда выполните

Вернуть обратно можно либо заново перегенерировав проект, либо выполните

Это снова включит случайную генерацию наборов данных в testbench.

Также вы можете захотеть изменить количество наборов данных для работы стенда. Тогда откройте файл sumn_sim_tb.v и в строке

укажите нужное вам количество повторений.

Кроме того в файле config.mcy в строке

установите нужное вам количество мутаций. Рекомендуется ~1000

Все настройки будут действительны только на текущий сеанс, пока вы не перегенерируете проект. См. пункт Как изменять

Работа с mcy

Почистите базу данных теста

Снова инициируйте новую базу данных

Выполните тесты

Иногда на мутациях бывает FAIL. Разберитесь и снова повторите

Второй путь

После того как вы развернёте проект, просто вызывайте mcy

Отображение статистики

После завершения mcy run вы получите что-то такое:

Уточнить покрытие можно командой

Положительные числа в левом столбце указывают на мутации, помеченные как COVERED, отрицательные числа указывают на UNCOVERED.

Также во время mcy run, в случае долгого теста вы можете выполнить в другом терминале и в корневом каталоге проекта

Откройте указанный адрес в своём браузере, чтобы следить за ходом выполнения на панели мониторинга. Это можно делать и при выполнении тестов на удалённом сервере.

Для более подробного визуального изучения мутаций можно открыть

Здесь вы увидите "горячие точки" вашего кода, где существуют пробелы в покрытии. На данный момент это жёстко запрограммировано для использования имён тегов «COVERED» и «UNCOVERED».

Как изменять

Вы можете вносить изменения в файлы: config.mcy, *.sv, *.v, *.sby, *.ys, *.sh кроме sumn. Но эти изменения будут текущими и не будут сохранены при выполнении sh sumn.

Если вы хотите фиксировать изменения то внесите изменения в sumn. Все файлы проекта будут перегенерированы при выполнении

а также при выполнении

Развивайте проект.