Спец курс (Избранные главы VHDL)/Верификация описания — различия между версиями
Материал из Wiki
Vidokq (обсуждение | вклад) (→Слайд:Верификация описания) |
Vidokq (обсуждение | вклад) (→Слайд:Верификация описания:step) |
||
| Строка 29: | Строка 29: | ||
** Assert'ы (psl, OVVM, UVM) | ** Assert'ы (psl, OVVM, UVM) | ||
** Отчеты и базы по результатам моделирования | ** Отчеты и базы по результатам моделирования | ||
| + | |||
| + | ==Слайд: Типы тестов ФК== | ||
| + | На что проверяем: | ||
| + | * {{Гол|'''<big>Детерминистский</big>'''}} - Проверяет обычные режимы работы системы, а также функционирование в граничных условиях на основе фиксированного набора тестов | ||
| + | * {{Гол|'''<big>Случайный</big>'''}} - Предполагает наличие генератора случайных входных воздействий | ||
| + | * {{Гол|'''<big>Транзакционный</big>'''}} - Фиксирует внимание на проверке интерфейсов и прохождению пакетов данных через них | ||
| + | |||
| + | Способ проведения проверки: | ||
| + | * {{Сн|'''<big>"Черный ящик"</big>'''}} | ||
| + | * {{Сн|'''<big>"Серый ящик"</big>'''}} | ||
| + | * {{Сн|'''<big>"Прозрачный ящик"</big>'''}} | ||
| + | |||
| + | ==Слайд: Полнота тестов == | ||
| + | |||
| + | * {{X|24px}}В реальных условия обычно полный перебор {{Кр|'''<big>невозможен</big>'''}} | ||
| + | * {{V|24px}}Поэтому поступают следующим образом. Например для сумматора: | ||
| + | # Тестируют как {{Фио|'''"Серый ящик"'''}} и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF | ||
| + | # Затем целенаправленно проверяют граничные условия - переполнение, перенос | ||
| + | # Затем тестирую как {{Фио|'''"Черный ящик"'''}} на случайном наборе тестов | ||
| + | # Оценивают полноту проверки модели | ||
| + | |||
| + | ==Слайд: Метрики оценки полноты тестов== | ||
| + | Необходимое условие : Управляемость (выполняется строка или переход) | ||
| + | Достаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном) | ||
| + | * {{Сн|'''<big>Эвристические метрики </big>'''}} - основанные на статистике появления ошибок | ||
| + | * {{Сн|'''<big>Программные метрики </big>'''}} | ||
| + | ** '''Полнота покрытия тестом строк кода модели''' | ||
| + | ** '''Полнота покрытия переходов''' (число пополнений ветвей оператора if и case ) | ||
| + | ** '''Полнота покрытия путей''' (все пути в графе программы) | ||
| + | ** '''Полнота покрытия выражений''' (оценка числа вычислений выражения по различных наборах) | ||
| + | ** '''Полнота переключений из 0 в 1 и из 1 в 0 каждого бита''' | ||
| + | * {{Сн|'''<big>Автоматно-метрический подход </big>'''}}(лучший вариант использовать формальную верификацию для автоматов) | ||
| + | * {{Сн|'''<big>Моделирование неисправностей </big>'''}}(в модель вносится неисправность) | ||
| + | * {{Сн|'''<big>Мониторинг событий</big>'''}} | ||
| + | |||
| + | == Слайд: Метрики в ModelSim == | ||
| + | {{V|24px}} В '''ModelSim''' для учета метрик покрытия при компиляции проекта нужно задать в меню '''Compile->Compiler option''' | ||
| + | |||
| + | <slides split="-----" width="600" > | ||
| + | [[Файл:Опции компиляции покрытия.jpg]] | ||
| + | |||
| + | </slides> | ||
==Слайд:Эталонная модель на языке ''{{Зел| <big>SystemC</big>}}''== | ==Слайд:Эталонная модель на языке ''{{Зел| <big>SystemC</big>}}''== | ||
Версия 12:55, 21 ноября 2012
- Заголовок
- Верификация описания.
- Автор
- Зайцев В.С.
- Нижний колонтитул
- Спец курс (Избранные главы 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)
- Отчеты и базы по результатам моделирования
Слайд: Типы тестов ФК
На что проверяем:
- Детерминистский - Проверяет обычные режимы работы системы, а также функционирование в граничных условиях на основе фиксированного набора тестов
- Случайный - Предполагает наличие генератора случайных входных воздействий
- Транзакционный - Фиксирует внимание на проверке интерфейсов и прохождению пакетов данных через них
Способ проведения проверки:
- "Черный ящик"
- "Серый ящик"
- "Прозрачный ящик"
Слайд: Полнота тестов
-
В реальных условия обычно полный перебор невозможен
-
Поэтому поступают следующим образом. Например для сумматора:
- Тестируют как "Серый ящик" и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF
- Затем целенаправленно проверяют граничные условия - переполнение, перенос
- Затем тестирую как "Черный ящик" на случайном наборе тестов
- Оценивают полноту проверки модели
Слайд: Метрики оценки полноты тестов
Необходимое условие : Управляемость (выполняется строка или переход) Достаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)
- Эвристические метрики - основанные на статистике появления ошибок
- Программные метрики
- Полнота покрытия тестом строк кода модели
- Полнота покрытия переходов (число пополнений ветвей оператора if и case )
- Полнота покрытия путей (все пути в графе программы)
- Полнота покрытия выражений (оценка числа вычислений выражения по различных наборах)
- Полнота переключений из 0 в 1 и из 1 в 0 каждого бита
- Автоматно-метрический подход (лучший вариант использовать формальную верификацию для автоматов)
- Моделирование неисправностей (в модель вносится неисправность)
- Мониторинг событий
Слайд: Метрики в ModelSim
В ModelSim для учета метрик покрытия при компиляции проекта нужно задать в меню Compile->Compiler option
Слайд:Эталонная модель на языке SystemC
- Высокий уровень абстракции
- Скорость моделирования
- Возможности языка C++
- Инструменты для автоматизации
- Совместное моделирование с другими HDL-языками
