Details

Title: Исследование и оптимизация решения задачи выполнимости булевых формул на базе реконфигурируемых аппаратных ускорителей: выпускная квалификационная работа магистра: направление 09.04.01 «Информатика и вычислительная техника» ; образовательная программа 09.04.01_20 «Проектирование компьютерных систем»
Creators: Осколков Владислав Сергеевич
Scientific adviser: Антонов Александр Петрович
Other creators: Новопашенный Андрей Гелиевич
Organization: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint: Санкт-Петербург, 2020
Collection: Выпускные квалификационные работы; Общая коллекция
Subjects: FPGA; SAT; OPENCL
Document type: Master graduation qualification work
File type: PDF
Language: Russian
Level of education: Master
Speciality code (FGOS): 09.04.01
Speciality group (FGOS): 090000 - Информатика и вычислительная техника
Links: Отзыв руководителя; Рецензия; Отчет о проверке на объем и корректность внешних заимствований
DOI: 10.18720/SPBPU/3/2020/vr/vr20-786
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Record key: ru\spstu\vkr\6156

Allowed Actions:

Action 'Read' will be available if you login or access site from another network Action 'Download' will be available if you login or access site from another network

Group: Anonymous

Network: Internet

Annotation

Тема выпускной квалификационной работы: «Исследование и оптимизация решения задачи выполнимости булевых формул на базе реконфигурируемых аппаратных ускорителей». Данная работа посвящена реализации на базе реконфигурируемого аппаратного ускорителя, используя стандарт OpenCL, решения задачи выполнимости булевых формул (задачи SAT), исследованию существующих вариантов реализации и их оптимизации с целью повышения эффективности. Задачи, которые решались в ходе исследования: проведение анализа существующих алгоритмов для решения задачи SAT, архитектурных особенностей современных реконфигурируемых ускорителей, возможностей инструментальных средств компании Xilinx, существующих аппаратных решений на базе SIMD и FPGA ускорителей; реализация решателя задачи SAT на базе реконфигурируемого аппаратного ускорителя Alveo компании Xilinx; проведение исследования, сравнительного анализа и оптимизации реализованного решателя, а также проведение сравнительного анализа созданного решателя с существующими реализациями решателя. При проведении исследования были использованы: имитационное моделирование с использованием возможностей пакета SDAccel компании Xilinx и сравнительный анализ результатов моделирования. В результате был реализован решатель задачи SAT и было произведено сравнение результатов моделирования, показавшее повышение эффективности решения задачи SAT, по сравнению с рассмотренными существующими решениями.

The subject of the graduate qualification work is “Research and optimization of the solution of the feasibility problem for Boolean formulas based on reconfigurable hardware accelerators”. The given work is devoted to the implementation on the basis of a reconfigurable hardware accelerator, using the OpenCL standard, to solve the feasibility problem of Boolean formulas (SAT problems), to study existing implementation options and their optimization in order to increase efficiency. Tasks that were solved during the study: analysis of existing algorithms to solve the SAT problem, architectural features of modern reconfigurable accelerators, the capabilities of Xilinx tools, existing hardware solutions based on SIMD and FPGA accelerators; implementation of the SAT problem solver based on Xilinx reconfigurable hardware accelerator Alveo; conducting research, comparative analysis and optimization of the implemented solver, as well as conducting a comparative analysis of the created solver with existing solver implementations. During the study, the following were used: simulation using the capabilities of the Xilinx SDAccel package and a comparative analysis of the simulation results. As a result, the SAT problem solver was implemented and the simulation results were compared, which showed an increase in the efficiency of solving the SAT problem, compared with the existing solutions considered.

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
External organizations N2 All Read
External organizations N1 All
Internet Authorized users SPbPU Read Print Download
Internet Authorized users (not from SPbPU, N2) Read
Internet Authorized users (not from SPbPU, N1)
-> Internet Anonymous

Usage statistics

stat Access count: 6
Last 30 days: 0
Detailed usage statistics