Донецкая Ю.В., Зыков А.Г., Поляков В.И. Методы верификации вычислительных процессов. Часть 1

СПб.: Университет ИТМО, 2019. — 142 с.Учебное пособие охватывает различные аспекты верификации вычислительных процессов, реализованных аппаратно, на уровне логических схем (часть 1) и программно (часть 2). В данной части приведено обоснование важности верификации проектов, даны определения формальной и функциональной верификаций вычислительных процессов, их валидации. Представлены теоретические основы методов верификации, таких, как основные положения теории множеств, булевой алгебры, теории графов и теории конечных автоматов. Подробно рассмотрены методы синтеза контролирующих тестов для функциональной верификации цифровых схем, включая формальные модели схем, построение комплексных покрытий и графов переходов, решение установочной задачи, синтез тестовых последовательностей и устранение статического риска сбоя. Рассмотрен вопрос формальной верификации моделей разного уровня представления.
Для закрепления теоретического материала предложены контрольные вопросы. Приведёны пример выполнения домашнего задания на синтез теста для последовательностной схемы и варианты заданий.
Учебное пособие предназначено для бакалавров широкого круга инженерных специальностей (проектирование вычислительных систем, программирование и др.), а также оно будет полезно для магистрантов, специализирующихся в области вычислительной техники.Предисловие.
Введение.
Верификация.
Место верификации при проектировании вычислительных систем.
Основные термины и определения.
Теоретические основы верификации вычислительных процессов.
Тестирование цифровых схем.
Содержание домашней работы.
Верификации цифровых схем.
Итерационно-рекурсивная модель последовательностной схемы.
Верификации моделей разного уровня методом построения графа переходов схемы.
Верификация моделей одного уровня абстракции.
Методы верификации цифровых схем.
Контрольные вопросы по темам «Тестирование и верификация цифровых схем».
Заключение.
Библиографический список.
Приложение. Устранение критических состязаний сигналов в логических схемах при реализации вычислительных процессов.
Приложение. Алгебро-топологическая модель последовательностной схемы в виде комплексного кубического покрытия.