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

Версия 15:55, 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

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

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

• Булева логика (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 с верификацией на основе утверждений