Спец курс (Избранные главы VHDL)/Верификация описания — различия между версиями

Версия 15:41, 21 ноября 2012

Slide Show

Заголовок

Верификация описания.

Автор

Зайцев В.С.

Нижний колонтитул

Спец курс (Избранные главы VHDL)/Верификация описания

Дополнительный нижний колонтитул

Зайцев В.С., 13:16, 2 декабря 2013

Слайд:Методы верификации проекта

• Имитационная верификация - верификация с использованием моделирования
• Формальная верификация -проверка модели с целью доказательства ее корректности и эквивалентности спецификации

(Пример: пакет FormulPro ф. MentorGraphics, пакеты фирмы Verplex, www.verplex.com)

Слайд:Верификация описания

Слайд:Верификация описания:step

• Среда моделирования
  • Active-HDL™
  • Riviera-PRO™
  • NC-Sim®
  • ModelSim®
  • QuestaSim®
  • VCS-MX®
• Структура проекта
  • Тестовое окружение
  • RTL-модель (Verilog,VHDL)
  • Эталонная модель (SystemC)
  • Assert'ы (psl, OVVM, UVM)
  • Отчеты и базы по результатам моделирования

Слайд:Средства верификации

• Прямые тесты (Directed tests)
• Псевдослучайные тесты (Random tests)
• Управляемые псевдослучайные тесты (Constrained Random tests)
• Верификация управляемая покрытием (на основе покрытия) (Coverage driven verification)
  • Покрытие кода (Code coverage)
  • Функциональное покрытие (Functional coverage )
• Верификация на основе утверждений (Assertion based verification)
• Эмуляция (Emulation)
• Формальная верификация (Formal verification)

Слайд: Типы тестов ФК

На что проверяем:

• Детерминистский - Проверяет обычные режимы работы системы, а также функционирование в граничных условиях на основе фиксированного набора тестов
• Случайный - Предполагает наличие генератора случайных входных воздействий
• Транзакционный - Фиксирует внимание на проверке интерфейсов и прохождению пакетов данных через них

Способ проведения проверки:

• "Черный ящик"
• "Серый ящик"
• "Прозрачный ящик"

Слайд:Что такое покрытие (Coverage)?

• Покрытие является крайне неоднозначным термином, когда используется сам по себе.

Покрытие в электронике (Coverage) является одной из разновидностей метрик проекта, которая сообщает, если определённые аспекты проекта были правильно выполнены во время процедуры тестирования.

• Обычно уточняют термин покрытия, говоря какой аспект был протестирован:
  • Тестирование качества кода — покрытие кода (code coverage)
  • Проверка свойств/утверждений — покрытие свойств/утверждений (property coverage)
  • Сбор значений переменных проекта — функциональное покрытие (functional coverage).

Слайд:Покрытие кода vs. функциональное покрытие

Слайд: Полнота покрытия

• В реальных условия обычно полный перебор невозможен
• Поэтому поступают следующим образом. Например для сумматора:

1. Тестируют как "Серый ящик" и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF
2. Затем целенаправленно проверяют граничные условия - переполнение, перенос
3. Затем тестирую как "Черный ящик" на случайном наборе тестов
4. Оценивают полноту проверки модели

Слайд: Метрики оценки полноты тестов

Необходимое условие : Управляемость (выполняется строка или переход)

Достаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)

• Эвристические метрики - основанные на статистике появления ошибок
• Программные метрики
• Автоматно-метрический подход (лучший вариант использовать формальную верификацию для автоматов)
• Моделирование неисправностей (в модель вносится неисправность)
• Мониторинг событий

Слайд: Эвристические метрики

• Календарное время между моментами обнаружения ошибок проекта (к концу процесса верификации оно увеличивается);
• Общее количество промоделированных тактов работы проектируемого устройства;
• Общее число обнаруженных ошибок в проекте и т.д.
• Число обнаруженных ошибок в день, неделю, месяц

Слайд: Программные метрики

• Полнота покрытия тестом строк кода модели
• Полнота покрытия переходов (число пополнений ветвей оператора if и case )
• Полнота покрытия путей (Branch coverage) (все пути в графе программы)
• Полнота покрытия выражений (Expression coverage) (оценка числа вычислений выражения по различных наборах)
• Полнота переключений из 0 в 1 и из 1 в 0 каждого бита (Toggle coverage)

Слайд: Метрики в ModelSim

В ModelSim для учета метрик покрытия при компиляции проекта нужно задать в меню Compile->Compiler option

Слайд: Виды покрытия кода в ModelSim

• Statement coverage — покрытие состояний

• Branch coverage — покрытие ветвлений

• Condition coverage — покрытие условий

• Expression coverage — покрытие выражений

• Toggle coverage — покрытие принимаемых значений

• FSM coverage — покрытие состояний автомата

Слайд: Мониторинг покрытия кода в ModelSim

Слайд: Команды ModelSim для работы с покрытием

Команда для компиляции

vcom +cover=bcsxf -work $wlibname $name

Ключевое слово +cover и после него строка из букв каждая из которых значит следующее:

1. b - покрытие ветвлений
2. c - покрытие условий
3. s - покрытие состояний
4. x - покрытие принимаемых битами значений ( 0\1\Z )
5. t - покрытие принимаемых битами значений ( 0\1 )
6. f - покрытие состояний конечного автомата

Слайд: Команды ModelSim для работы с покрытием

Слайд: Команды ModelSim для работы с покрытием

Для запуска моделирования с покрытием нужно включить следующие опции:

Simulate->Start Simulation на закладке other поставить птичку enable code coverage

Команда для компиляции

vsim -coverage 

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

coverage save -onexit