«Работать добросовестно — значит: работать, повышая свою квалификацию, проявляя инициативу в совершенствовании продукции, технологий, организации работ, оказывая не предусмотренную должностными инструкциями помощь другим сотрудникам (включая и руководителей) в общей им всем работе.

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

Материал из Wiki
Перейти к: навигация, поиск
(→‎Слайд:Средства верификации)
(→‎Слайд: Метрики в ModelSim)
Строка 40: Строка 40:
 
* {{Сн|'''<big>"Серый ящик"</big>'''}}
 
* {{Сн|'''<big>"Серый ящик"</big>'''}}
 
* {{Сн|'''<big>"Прозрачный ящик"</big>'''}}
 
* {{Сн|'''<big>"Прозрачный ящик"</big>'''}}
−
 
−
== Слайд:Средства верификации ==
 
−
 
−
* Прямые тесты (Directed tests)
 
−
* Псевдослучайные тесты (Random tests)
 
−
* Управляемые псевдослучайные тесты (Constrained Random tests)
 
−
* Верификация управляемая покрытием (на основе покрытия) (Coverage driven verification)
 
−
** Покрытие кода (Code coverage)
 
−
** Функциональное покрытие (Functional coverage )
 
−
* Верификация на основе утверждений (Assertion based verification)
 
−
* Эмуляция (Emulation)
 
−
* Формальная верификация (Formal verification)
 
−
 
−
== Слайд:Что такое покрытие (Coverage)? ==
 
−
 
−
* Покрытие является крайне неоднозначным термином, когда используется сам по себе.
 
−
 
−
Можно сказать, что (в электронике):
 
−
 
−
{{Info |'''Покрытие''' ('''''Coverage''''') является одной из разновидностей метрик проекта, которая сообщает, если определённые аспекты проекта были правильно выполнены во время процедуры тестирования.}}
 
−
 
−
* Обычно уточняют термин покрытия, говоря какой аспект был протестирован:
 
−
** Тестирование качества кода — покрытие кода (code coverage)
 
−
** проверка свойств/утверждений — покрытие свойств/утверждений (property coverage)
 
−
** Сбор значений переменных проекта — функциональное покрытие (functional coverage).
 
−
 
−
== Слайд:Покрытие кода vs. функциональное покрытие==
 
−
 
−
[[Файл:Code quality-vs-functionality.png|center|400px]]
 
  
 
==Слайд: Полнота тестов ==
 
==Слайд: Полнота тестов ==
Строка 83: Строка 54:
 
Достаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)
 
Достаточное условие : Наблюдаемость (результат исполнения влияет на выход сравниваемый с эталоном)
 
* {{Сн|'''<big>Эвристические метрики </big>'''}} - основанные на статистике появления ошибок
 
* {{Сн|'''<big>Эвристические метрики </big>'''}} - основанные на статистике появления ошибок
−
** календарное время между моментами обнаружения ошибок проекта (к концу процесса верификации оно увеличивается);
 
−
** общее количество промоделированных тактов работы проектируемого устройства;
 
−
** общее число обнаруженных ошибок в проекте и т.д.
 
 
* {{Сн|'''<big>Программные метрики </big>'''}}
 
* {{Сн|'''<big>Программные метрики </big>'''}}
 
** '''Полнота покрытия тестом строк кода модели'''
 
** '''Полнота покрытия тестом строк кода модели'''
 
** '''Полнота покрытия переходов''' (число пополнений ветвей оператора if и case )
 
** '''Полнота покрытия переходов''' (число пополнений ветвей оператора if и case )
−
** '''Полнота покрытия путей ''(Branch coverage)''''' (все пути в графе программы)
+
** '''Полнота покрытия путей''' (все пути в графе программы)
−
** '''Полнота покрытия выражений ''(Expression coverage)''''' (оценка числа вычислений выражения по различных наборах)
+
** '''Полнота покрытия выражений''' (оценка числа вычислений выражения по различных наборах)
−
** '''Полнота переключений из 0 в 1 и из 1 в 0 каждого бита ''(Toggle coverage)'''''
+
** '''Полнота переключений из 0 в 1 и из 1 в 0 каждого бита'''
 
* {{Сн|'''<big>Автоматно-метрический подход </big>'''}}(лучший вариант использовать формальную верификацию для автоматов)
 
* {{Сн|'''<big>Автоматно-метрический подход </big>'''}}(лучший вариант использовать формальную верификацию для автоматов)
 
* {{Сн|'''<big>Моделирование неисправностей </big>'''}}(в модель вносится неисправность)
 
* {{Сн|'''<big>Моделирование неисправностей </big>'''}}(в модель вносится неисправность)
 
* {{Сн|'''<big>Мониторинг событий</big>'''}}
 
* {{Сн|'''<big>Мониторинг событий</big>'''}}
  
−
== Слайд: Метрики в ModelSim ==
+
== Слайд: Включение контроля метрик в ModelSim ==
 
{{V|24px}} В '''ModelSim''' для учета метрик покрытия при компиляции проекта нужно задать в меню '''Compile->Compiler option'''
 
{{V|24px}} В '''ModelSim''' для учета метрик покрытия при компиляции проекта нужно задать в меню '''Compile->Compiler option'''
  
 
<slides split="-----" width="600" >
 
<slides split="-----" width="600" >
−
[[Файл:Опции компиляции покрытия.jpg|center]]
+
[[Файл:Опции компиляции покрытия.jpg]]
  
 
</slides>
 
</slides>
−
 
+
== Слайд: Метрики в ModelSim ==
−
== Слайд: Виды покрытия кода в 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.
+
  
 
==Слайд:Эталонная модель на языке ''{{Зел| <big>SystemC</big>}}''==
 
==Слайд:Эталонная модель на языке ''{{Зел| <big>SystemC</big>}}''==

Версия 14:24, 21 ноября 2012

Slide Show
Slide Show
Заголовок
Верификация описания.
Автор
Зайцев В.С.
Нижний колонтитул
Спец курс (Избранные главы VHDL)/Верификация описания
Дополнительный нижний колонтитул
Зайцев В.С., 13:16, 2 декабря 2013

[на всё окно]

Содержание

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

  • Имитационная верификация - верификация с использованием моделирования
  • Формальная верификация -проверка модели с целью доказательства ее корректности и эквивалентности спецификации 
(Пример: пакет FormulPro ф. MentorGraphics, пакеты фирмы Verplex, www.verplex.com)


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

Процевв верификации.png

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

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

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

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

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

  • Nuvola apps error.pngВ реальных условия обычно полный перебор невозможен
  • 200px-Yes check.pngПоэтому поступают следующим образом. Например для сумматора:
  1. Тестируют как "Серый ящик" и проверяют простейшие случаи 0+0, 0+1, FFFF+FFFF, 0+FFFF
  2. Затем целенаправленно проверяют граничные условия - переполнение, перенос
  3. Затем тестирую как "Черный ящик" на случайном наборе тестов
  4. Оценивают полноту проверки модели

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

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

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

Слайд: Включение контроля метрик в ModelSim

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

Опции компиляции покрытия.jpg

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

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

  1. Высокий уровень абстракции
  2. Скорость моделирования
  3. Возможности языка C++
  4. Инструменты для автоматизации
  5. Совместное моделирование с другими HDL-языками
Источник — «http://www.simhard.com/wiki/index.php?title=Спец_курс_(Избранные_главы_VHDL)/Верификация_описания&oldid=397»