Бибило П.Н., Авдеев Н.А., Романов В.И. Функциональная верификация VHDL-описаний синхронных цифровых устройств

Оглавление

Введение.........................................................................................5

Глава 1. Средства моделирования для функциональной верификации синхронных цифровых устройств..................7

1.1. Спецификации на проектирование и VHDL-описания цифровых устройств........................................................................7

1.2. VHDL-модели и тестирующие программы.................................17

1.3. Система Questa Sim. Моделирование с помощью скриптов......22

1.4. Генерация псевдослучайных тестов.............................................27

1.5. Покрытие VHDL-кода....................................................................58

Глава 2. Верификация VHDL-описаний комбинационной логики.........................................................66

2.1. VHDL-описания систем полностью определенных булевых функций...........................................................................66

2.2. VHDL-описания систем неполностью определенных булевых функций...........................................................................79

2.3. Структурные описания комбинационных логических схем...........................................................................105

2.4. Алгоритмические описания блоков комбинационной логики..............................................................109

2.5. Перепроектирование комбинационных логических схем ........ 114

Глава 3. Верификация VHDL-описаний логических

схем с памятью и конечных автоматов...............................130

3.1. Структурные описания логических схем с элементами памяти....................................................................130

3.2. VHDL-описания конечных автоматов........................................140

3.3. Задача нахождения цикла в ориентированном графе...............171

3.4. Нахождение энергоемких тестов для логических схем, реализующих конечные автоматы..............................................185

Глава 4. Верификация VHDL-описаний сетей синхронных конечных автоматов........................................205

4.1. Операционное устройство - композиция конечного автомата и арифметико-логического устройства......................................205

4.2. Сеть конечных автоматов с общими входами...........................224

Глава 5. Верификация и схемная реализация

VHDL-описаний параллельных алгоритмов логического управления.........................................................254

5.1. Параллельные автоматы..............................................................255

5.2. Верификация параллельных автоматов.....................................261

5.3. Синхронная VHDL-модель параллельного автомата...............268

5.4. Секвенциальный автомат............................................................284

5.5. Представление сети автоматов в виде одного параллельного автомата..............................................................292

5.6. Функциональные возможности программы QPralu.................303

Заключение................................................................................314

Список основных сокращений и имен.................................315

Литература................................................................................318

Введение

Проблема верификации исходных спецификаций цифровых устройств и систем, реализуемых на цифровых сверхбольших интегральных схемах (СБИС), является в настоящее время одной из важнейших для проектировщиков цифровой аппаратуры и разработчиков систем автоматизированного проектирования (САПР). В данной книге в качестве верифицируемых проектов цифровых устройств рассматриваются их VHDL-описания, а под верификацией понимается проблема проверки соответствия VHDL-описаний спецификациям на проектирование. Язык VHDL широко используется в качестве языка исходного описания проектов при создании разнообразной электронной аппаратуры на современной элементной базе СБИС, таких как заказные цифровые СБИС, системы-на-кристалле и программируемые логические интегральные схемы (ПЛИС). Выбор класса синхронных схем обусловлен тем, что современные системы синтеза (синтезаторы) логических схем реализуют функциональные VHDL-описания в виде синхронных логических схем в заданных библиотеках проектирования.

Описываемые в книге средства функциональной верификации VHDL-описаний синхронных цифровых устройств базируются на моделировании - основном, используемом на практике направлении верификации, для чего применяются соответствующие системы моделирования. В качестве системы моделирования всех представленных в книге VHDL-описаний использовалась система Questa Sim (ф. Mentor Graphics). Выбор данной системы обусловлен не только ее широким распространением, но и тем, что в ней имеются средства для анализа покрытия VHDL-кодов при моделировании; кроме того, в ней можно проверять истинность ассертов - строгих утверждений о функциональных свойствах проекта.

В книге рассматриваются VHDL-модели синхронных цифровых устройств и методики их функциональной верификации. Основное внимание уделяется верификации VHDL-описаний блоков управляющей логики и функциональных блоков, реализующих арифметико-логические устройства. Рассматривается генерация управляемых псевдослучайных тестов. Предлагаются программные средства формирования (по результатам верификации блоков проекта) компактных функциональных тестов, которые требуются для проведения комплексной верификации всего проекта в целом. Такая верификация осуществляется после выполнения независимой верификации блоков VHDL-проекта.

Рассматриваются способы описания и верификация комбинационных блоков с неопределенностью поведения, функционирование таких блоков описывается системами неполностью определенных логических функций.

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

При изложении материалов предполагается, что читатели знакомы с основами языка VHDL в рамках стандартов VHDL'1993, VHDL'2008 и имеют определенные знания, требуемые для разработки моделей цифровых устройств. Заметим, что последние стандарты VHDL и соответствующие VHDL-пакеты во многом ориентированы на верификацию и открывают новые возможности для моделирования и верификации VHDL-описаний цифровых устройств. Полезным при чтении данной книги будет знакомство также с материалами сайта www.bsuir.by/vhdl/, посвященного языку VHDL, на котором размещены различные методические материалы и примеры VHDL-программ.

Номера рисунков, таблиц, листингов, формул «привязаны» к номеру соответствующего раздела книги.

Об авторах

Бибило Петр Николаевич

Доктор технических наук, профессор. Его основные научные работы относятся к теории дискретных устройств и автоматизации проектирования дискретных устройств и цифровых сверхбольших интегральных схем (СБИС), применению методов искусственного интеллекта в системах автоматизированного проектирования (САПР). Считает, что успешное развитие микроэлектроники связано с разработкой и внедрением в практику проектирования новых архитектур САПР, использующих экспертные знания о маршрутах и объектах проектирования. Уделяет большое внимание подготовке студентов и специалистов-разработчиков, читает курсы лекций в Белорусском государственном университете информатики и радиоэлектроники, является инициатором создания русскоязычного Интернет-сайта по языку VHDL.

Авдеев Николай Александрович

Кандидат технических наук. Его основные научные интересы связаны с разработкой проектов цифроаналоговых микросхем, методами синтеза логических схем в различных технологических базисах, а также средствами верификации проектов СБИС на основе современных информационных технологий проектирования.

Романов Владимир Ильич

Кандидат технических наук, доцент. Его основные научные интересы связаны с разработкой инструментария для решения задач логико-комбинаторного характера, разработкой программного обеспечения САПР дискретных устройств и применения в них методов искусственного интеллекта. В Белорусском государственном университете информатики и радиоэлектроники читает курс лекций «Проектирование программ в интеллектуальных системах».