Вы здесь

Логическая верификация аппаратуры


п/п
Название модулей Разделы и темы лекционных занятий Содержание Аудиторная работа (зачетные ед./часы)

1

I.

Основные методы верификации

Место верификации в маршруте проектирования.

Процесс проектирования для asic (БИС/СБИС).
Процесс проектирования для fpga (ПЛИС).

2

2

Базовые принципы верификации

Верификация на основе  моделирования (simulation-based).
Формальная верификация.
Гибридные методы.
Логическая верификация и верификация временных характеристик.
Цикл верификации.
Черный, белый, серый ящики и спецификация.

2

3

II.

Верификация на основе  моделирования

Моделирование RTL с точки зрения верификации

Языки описания аппаратуры.
Два основных подхода к моделированию их достоинства и недостатки:
-События
-Опрос в цикле
Компиляторы и интерпретаторы (vcs,modelsim).
Проблема неоднозначной интерпретации конструкций verilog.
4-state и 2-state моделирование.
Моделирование gate-verilog с задержками. sdf-формат.
Проблема моделирования с учетом X-состояния

4

4

Стандарты интерфейса RTL-модели с внешним ПО. VPI.

Программные интерфейсы взаимодействия с внешним ПО. История существующих стандартов (PLI 1.0 (ACC/TF), PLI 2.0 (VPI), DPI). Примеры применения.
Структура и основные шаги процесса создания VPI-приложения. Описание PLI-интерфейса: calltf, compiletf, sizetf, callback-процедуры. Регистрация функций и процедур VPI-приложения. Обзор VPI-библиотеки. Доступ к элементам моделируемой системы (чтение и модификация). Синхронизация внешнего приложения с моделью. Пример VPI-приложения.

4

5

DPI как новый этап развития интерфейсов программного взаимодействия.

Обзор: задачи и функции, типы данных. Уровни DPI: уровень SystemVerilog и уровень внешнего языка. Импортируемые программные модули и  функции: накладываемые требования, объявление и возвращаемые значения. Типы формальных аргументов. Изолированные (pure) и контекстные (context) функции. Вызов импортируемых функций. Экспортируемые программные модули и функции.

4

6

Современные методологии построения тестового окружения.

Обзор современных методологий и библиотек для построения тестовых окружений. Библиотеки и методологии на основе SystemVerilog (VMM, OVM, UVM). Базовая структура тестового окружения по OVM.
Обзор доступных компонентов библиотеки OVM. Реализация тестовых последовательностей средствами OVM. Виртуальные секвенсоры и реализация многоуровневых тестовых последовательностей. Система фаз теста.
Верификация с помощью утверждений (Assertion Based Verification). Обзор языков описания свойств системы — PSL, SystemVerilog Assertions (SVA).
Описание функционального покрытия средствами SystemVerilog.

4

7

Оценка полноты верификации.

Проблема оценки качества верификации. Понятие тестового покрытия, его роль в верификации. Понятие метрики покрытия 
Классификация метрик: явные и неявные, синтаксические и семантические, основанные на спецификации и реализации. Проблема измеримости метрики.
Метрики, основанные на частоте обнаружения ошибок.
Метрики покрытия исходного RTL-кода.
Метрики покрытия оборудования 
Покрытие проверок свойств

6

8

III.

Формальная верификация

Методы формальной верификации.

Введение в проблематику формальной верификации.
Область применения.
Основные алгоритмы, используемые в инструментах для формальной верификации.
Применение формальных методов для верификации конечных автоматов.
Проверка эквивалентности.
Проверка свойств.

6

9

Гибридные методы верификации

Верификация с использованием assertions.
Гибридные (полуформальные) методики верификации.
Символьное моделирование.
Применение формальных методов для улучшения  метрик моделирования.

2