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

Версия 13:19, 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)

Слайд: Полнота тестов

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

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 — counts the execution of each statement on a line individually, even if there are multiple statements in a line.

• Branch coverage — counts the execution of each conditional “if/then/else” and “case” statement and indicates when a true or false condition has not executed.

• Condition coverage — analyzes the decision made in “if” and ternary statements and can be considered as an extension to branch coverage.

• Expression coverage — analyzes the expressions on the right hand side of assignment statements, and is similar to condition coverage.

• Toggle coverage — counts each time a logic node transitions from one state to another.

• FSM coverage — counts the states, transitions, and paths within a finite state machine.

Слайд:Эталонная модель на языке SystemC

1. Высокий уровень абстракции
2. Скорость моделирования
3. Возможности языка C++
4. Инструменты для автоматизации
5. Совместное моделирование с другими HDL-языками