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

Текущая версия на 13:16, 2 декабря 2013

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

Слайд: Верификация на основе утверждений

Позволяет контролировать:

• Булева логика (Boolean logic) - тестирует основные утверждения (statements) о проекте.
• Временная логика (Temporal logic) - добавляет временное измерение (dimension) в булеву логику (Boolean logic) и тестирует отсутствие (absence), наличие (presence), неизменность/повторяемость (persistence), последовательность (sequence), и прочее определённых событий.
• Свойства/утверждения (Property) - это формальное описание поведения проекта, взятое из спецификации проекта и выраженное в терминах временной логики (temporal logic).

Могут быть выражены с помощью PSL (Property Specification Language – теперь включен в VHDL) или с помощью SVA (подмножество SystemVerilog Assertions – работает с VHDL через модули проверок (checker modules)).

• Последовательности (Sequences) являются простейшей формой свойств/утверждений, представляющие последовательность событий/состояний.\

Assertions – работает с VHDL через модули проверок (checker modules)).

Слайд: Пример верификации на основе утверждений

• Можно вставлять PSL код в специальные комментарии в VHDL; таким образом, этот код не будет оказывать влияния на синтез и похожие программы.
• Можно задать последовательности (sequences) для представления разных фаз задаваемого свойства.
• Конечное описания свойства (property) объединяет эти последовательности.
• Помеченная меткой директива cover показывает симулятору, как проверять это свойство.

--@clk  rising_edge(CLK);
--@psl  sequence ack35_s is { rose(ACK) : (ACK='1')[*3 to 5] } ;
--@psl  sequence dvalid24_s is { rose(DVALID) : (DVALID='1')[*2 to 4] } ;
--@psl  sequence dvalid2inf_s is { fell(ACK) : (DVALID='1')[*2 to inf] } ;
--@psl  property ackdvalid_p is { ack35_s ; dvalid24_s ; dvalid2inf_s } ;
--@psl  ackdvalid_c: cover(ackdvalid_p) report "Sequence ACK/DVALID covered!";

Слайд: Запуск моделирования в ModelSim с верификацией на основе утверждений

Для компиляции проекта содержащего файл верификации утверждений выполняем команду:

vcom -93 DIGITAL_BLOCK.vhd -pslfile DIGITAL_PSL.psl

После параметра -pslfilee указываем имя или путь к файлу

Для запуска моделирования проекта содержащего файл верификации утверждений выполняем команду:

vsim имя_проекта 

Для отключения выполнения проверок используем параметр -nopsl

vsim имя проекта -nopsl 

Слайд: Быстродействие и расход памяти

Кроме полноты тестирования, одной из важных характеристик тестирующей программы являются:

• Требуемая память
• Расход машинного времени

Слайд: Требуемая память

• Зависит от числа данных в программе
• Их размера (размерности)
• От количества и сложности операторов

Пример:

Данные типа signal в VHDL занимают на порядок!! больше места, чем variable, поэтому массивы данных большого объема в тестирующих модулях лучше объявлять с использованием variable.

Verilog расходует обычно в 4 раза меньше памяти на хранение одного бита данных, чем VHDL.

Слайд: Сокращение расхода машинного времени

1. Профилирование - эффективня организация тестирующей программы
2. Использование систем и языков предназначенных для верификации
3. Выбор более быстрой системы моделирования (вместо интерпретатора компилятор)
4. Использование более мощной ЭВМ
5. Ограничение множества входных наборов тестов (нет ничего мощнее здравого смысла)
6. Использование аппаратных ускорителей моделирования (10-100раз)
7. Использование прототипов схем для прогонов тестов (на этапе отладки тестов)

Пример:

1. Три отдельных процесса требуют больше времени, чем те же операции объединенные в один процесс.

2. Использование языков C,C++,SystemC позволяет не несколько раз снизить расход памяти