№ п/п |
Название модулей | Разделы и темы лекционных занятий | Содержание | Аудиторная работа (зачетные ед./часы) |
---|---|---|---|---|
1 |
I. Основные методы верификации |
Место верификации в маршруте проектирования. |
Процесс проектирования для asic (БИС/СБИС). |
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. |
4 |
|
7 |
Оценка полноты верификации. |
Проблема оценки качества верификации. Понятие тестового покрытия, его роль в верификации. Понятие метрики покрытия Классификация метрик: явные и неявные, синтаксические и семантические, основанные на спецификации и реализации. Проблема измеримости метрики. Метрики, основанные на частоте обнаружения ошибок. Метрики покрытия исходного RTL-кода. Метрики покрытия оборудования Покрытие проверок свойств |
6 |
|
8 |
III. Формальная верификация |
Методы формальной верификации. |
Введение в проблематику формальной верификации. |
6 |
9 |
Гибридные методы верификации |
Верификация с использованием assertions. Гибридные (полуформальные) методики верификации. Символьное моделирование. Применение формальных методов для улучшения метрик моделирования. |
2 |