Заключение диссертационного совета (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов)

1Аттестационное дело №_____07.12.2017 г. протокол № 58Заключение диссертационного совета Д 212.131.05, созданного на базефедеральногогосударственногобюджетногообразовательногоучреждения высшего образования «Московский технологическийуниверситет» (МИРЭА), Министерства образования и науки РоссийскойФедерации, находящейся по адресу 119454, Москва, проспектВернадского, д.78, номер приказа № 651-687 от 19 ноября 2010 г., подиссертации Быкова Сергея Анатольевича на соискание ученой степеникандидата технических наук по специальности 05.13.11 – Математическоеи программное обеспечение вычислительных машин, комплексов икомпьютерных сетейДиссертация «Исследование и разработка методов автоматическоговывода геометрических ограничений с использованием декларативногопрограммирования и формальных методов» в виде рукописи поспециальности 05.13.11 – «Математическое и программное обеспечениевычислительных машин, комплексов и компьютерных сетей» выполнена вфедеральном государственном автономном образовательном учреждениивысшегообразования(государственный«Московскийуниверситет)»нафизико-техническийкафедреинститут«Микропроцессорныетехнологии в интеллектуальных системах управления».

Диссертацияпринята к защите 29.06.2017 г., протокол 9-7/Р.Соискатель Быков Сергей Анатольевич, 1988 г. рожд., гражданинРФ, основное место работы на момент защиты Acronis Singapore R&D вдолжности научного сотрудника. В 2010 г. Быков С.А. закончилбакалавриат по направлению «Информатика и вычислительная техника», ав 2012 г. магистратуру по тому же направлению в федеральномгосударственном бюджетном образовательном учреждении высшегопрофессиональногообразования«Волгоградскийгосударственныйтехнический университет». С 2013 г. по 2017 г Быков С.А.

проходилподготовкуавтономноговочнойаспирантуреобразовательногофедеральногоучреждениягосударственноговысшегообразования2«Московскийфизико-техническийинститут(государственныйуниверситет)». Удостоверение о сдачи кандидатских экзаменов выдано в2016 г. федеральным государственным автономным образовательнымучреждением высшего образования «Московский физико-техническийинститут (государственный университет)».Научныйруководитель–РыженкоНиколайВладимирович,кандидат технических наук, ведущий научный сотрудник Intel Corporation.Официальные оппоненты: Бычков Игнат Николаевич, гражданинРФ, доктор технических наук, заместитель генерального директора ПАО«ИНЕУМ им.

И.С. Брука», г. Москва, Путря Федор Михайлович,гражданин РФ, кандидат технических наук, начальник лаборатории«ВерификацииСнКиIP-блоков»НТО-1,АОНПЦ«ЭЛВИС»,г. Зеленоград, дали положительные отзывы о диссертации. Ведущаяорганизация федеральное государственное учреждение «ФедеральныйнаучныйцентрисследованийНаучно-исследовательскийРоссийскойакадемиинаук»институтдаласистемныхположительноезаключение о диссертации (заключение составлено Евлампиевым Б.Е.,заведующимотделомМоисеевым А.С.,топологическоговедущимнаучнымпроектирования,сотрудником,икандидатомтехнических наук, доцентом, утверждено директором ФГУ ФНЦ НИИСИРАН, доктором технических наук, Бобковым С.Г.).Выборофициальныхобосновываетсяналичиемихоппонентовкомпетентностьюпубликацийивспособностьюиведущейорганизациирассматриваемойопределитьотрасли,научнуюипрактическую ценность диссертации.На диссертацию и автореферат поступило 6 положительныхотзывов:1.От к.

ф.-м. н., доцента кафедры вычислительной физикиСанкт-Петербургского государственного университета Немнюгина С.А.,3замечания: 1) отсутствуют ссылки на работы других авторов, заисключением ссылок на работы Suto et.al. (2012) и Tseitin et.al. (1983);2) отсутствует сравнение эффективности разработанных методов иалгоритмов с представленными в литературе.2.Отк.т.н.,доцентакафедры17национальногоисследовательского ядерного университета «МИФИ» Сафонова И.В.,замечание: в автореферате опущены вопросы, связанные с оценкойвремени работы разработанного программного комплекса и особенностейего программной реализации для различных вычислительных платформ.3.От к. ф.-м.

н., доцента кафедры информационных систем икомпьютерногоуниверситетамоделированияКузьминаН.М.,Волгоградскогозамечания:1)государственногоотсутствуетсписоклитературы, 2) в публикациях автора по теме диссертации отсутствуетссылка на свидетельство о регистрации программы для ЭВМ. Кроме того,в автореферате описаны только математическая модель и алгоритмавтоматическоговыводагеометрическихограничений;описаниясобственно программного обеспечения нет.4.Отк.ф.-м.н.,руководителяпроектаНаучно-исследовательский центр компании «Шлюмберже» Якимчука И.В.,замечание: комментируя результаты работы автор использует достаточнообщуюфразу«Приработеспромышленнымипроцессами,описывающими на порядки больше технологических ограничений,выигрыш по площади может быть иным».

Хотелось бы увидеть болееконкретные оценки: на сколько порядков больше технологическихограничений? Ожидается ли увеличение или уменьшение выигрыша поплощади?5.Отзаведующегокафедрой«Электронно-вычислительныемашины и системы» ФГБОУ ВО «Волгоградский государственныйтехнический университет», к.т.н., Андреева А.Е. и от доцента этой же4кафедры, к.т.н., Скакунова В.Н., замечания: 1) Неточности в определенииположений, выносимых на защиту, а также научной новизны. Вположениях, как правило, отмечаются предлагаемые методы, способы,подходы, но не алгоритмы, их реализующие, и тем более невычислительный комплекс.

В п.3 научной новизны указано столькопризнаков, что выделить основной, составляющий новизну, вообщезатруднительно. В целом формулировка п.3 неудачна, предложение в п. 3не согласовано. 2) Автореферат содержит много грамматических истилистических ошибок, затрудняющих однозначное понимание текста.Так, уже отмечено несогласованное предложение в п.3 научной новизны, втаблице 1, видимо, не выделена одна из строк, соответствующая значениюout=0, перепутаны подписи д) и г) к рисунку 12.

Отдельно можно отметитьсписок публикаций, где стоило бы объединить ссылки 3 и 4, а в пп. 5 и 9уточнить библиографические сведения. 3) в автореферате, как один изосновных результатов, выделен вычислительный комплекс. Однако нераскрыта полная структура комплекса, функции, связи и взаимодействиекомпонентов комплекса.

Описания отдельных алгоритмов и их схемдополнительной ясности не вносят. 4) При описании разработанныхавтором алгоритмов и предлагаемых подходов недостаточно явновыделены и недостаточно подробно рассмотрены их отличия от ранееизвестных.6.Отк.ф.-м.н.,конструированиядоцентаинтегральныхкафедрымикросхемпроектированияиНациональногоисследовательского университета «Московского института электроннойтехники», Матюшкина И.В., г. Зеленоград, замечания: 1) в названиидиссертациивынесено«…декларативногопрограммирования».Направление движения можно приветствовать, но если использовалисьимеющиеся языки программирования, то какие? А если был разработанновый, свой язык программирования, то каковы его синтаксические5диаграммы и лексемы? Сложилось впечатление, что авторы остановилисьгде-то в середине пути.

Хотя повторяю – направление теоретическихисследований представляется весьма интересным, коррелирующим свозрождающимися рекурсивными, функционально-логическими методамипрограммирования в целом. В списке публикаций авторы используютболее скромную и более точную отсылку к булевым формулам. 2) длявынесенноговрезультатыдиссертацииперечислениямножествагеометрических ограничений не проведено исследования его временнойсложности (линейный, квадратичный и т.д.). Также хотелось бы видеть иоценки структурной сложности. Хотя, как мне кажется, для полученияпорядка сложности потребуются нестандартные методы. 3) в текстеавторефератанетссылокнавнешнююлитературу,например,описывающую метод AllSAT или метод Цейтина.

4) если действительнобыл разработан вычислительный комплекс (Положение №4), уместнобыло бы дать его описание – хотя бы в виде какой-либо UML- диаграммы,что отсутствует в автореферате.Соискателем по теме диссертации опубликованы 8 работ, 6 - вжурналах, входящих в Перечень российских рецензируемых научныхизданий, в которых должны быть опубликованы основные научныерезультаты диссертаций на соискание ученых степеней доктора икандидата наук:1.Минимизациячисланежелательныхтопологийприпроектировании стандартных ячеек / Быков С.А., Рыженко Н.В., СорокинА.А., Талалай М.С.

// Проблемы разработки перспективных микро- инаноэлектронных систем -2014. Сборник трудов. — 2014. — № 1. — С.121–136.2.С.А. Быков, Н.В. Рыженко, А.А. Сорокин. Синтез блоковпамяти с использованием представления правил в виде булевых функцийот топологических объектов // Проблемы разработки перспективных6микро- и наноэлектронных систем - 2014. Сборник трудов.

— 2014. — №1. — С. 127 –132.3.Minimization of undesired layout patterns during standard cellsynthesis / Bykov S.A., Ryzhenko N.V., Sorokin A.A., Talalay M.S. //Проблемы разработки перспективных микро- и наноэлектронных систем(МЭС). —2015. — no. 1. — P. 29.4.S.A. Bykov, N.V. Ryzhenko, A.A. Sorokin. Synthesis of memoryunits using a description of design rules via Boolean functions of layout objects// Проблемы разработки перспективных микро- и наноэлектронных систем(МЭС).

— 2015. — no. 1. — Pp. 30–31.5.С.А. Быков, Н.В. Рыженко, А.А. Сорокин. Автоматическийвывод дополнительных ограничений на границах стандартных ячеек //Проблемы разработки перспективных микро- и наноэлектронных систем(МЭС). — 2016. — № 1. — С. 137–143.6.Н.В. Рыженко, А.А. Сорокин, С.А. Быков. Трассировкабитовых элементов памяти с автоматическим построением ограничений награницах ячеек // Проблемы разработки перспективных микро- инаноэлектронных систем (МЭС). — 2016.

— № 1. — С. 144–150.7.БыковС.А.Практическиеприложениязадачиовыполнимости булевых формул // Т. 3: Информационные технологии имоделирование процессов в технике. — НИЦ ИНФРА-М, 2015. — С. 77–79.8.S.A. Bykov, N.V. Ryzhenko, A.A. Sorokin. Automated Solutionfor Preventing Design Rules Violations at Abutment Stage for Standard CellsSynthesis Flow // 14th IEEE East-West Design & Test Symposium (EWDTS2016). — IEEE, 2016.Диссертационный совет отмечает, что на основании выполненныхсоискателемгеометрическихисследованийограниченийразработаннаграницахалгоритмструктурныхпостроенияэлементов7ограниченной площади, заключающийся в перечислении всех геометрий,удовлетворяющихзаданнымгеометрическимограничениям,ивформировании групп геометрий, не приводящих к возникновениюнарушений геометрических ограничений на границах структурныхкомпонентов;разработаналгоритмоценкикачестваполученныхгеометрических ограничений на границах структурных компонентовограниченной площади, заключающийся в построении тестового наборакомпонентовсучетомполученныхгеометрическихограниченийи минимизации их суммарной площади методом «ветвления и границ»;доказанаэффективностьпрограммированияииспользованияформальныхметодовдлядекларативногорешениязадачмногопараметрической оптимизации большой размерности; разработанвычислительный комплекс «Вычислитель геометрических ограничений».Теоретическая значимость исследования обосновано тем, что даноформальное описание задачи формирования геометрических ограниченийна границах структурных компонентов ограниченной площади, раскрытыпроблемные аспекты применения имеющихся подходов в областипредотвращения возникновения нарушений геометрических ограниченийнаграницахструктурныхкомпонентов;разработаналгоритмформирования субоптимального набора геометрических ограничений награницах структурных компонентов, основанный на использованиидекларативного программирования и формальных методов.

Теоретическиерезультаты диссертационного исследования коррелируют с современнымирезультатами зарубежных и отечественных авторов.Практическоеподтверждаетсязначениетем,чтообеспечениекомплексаограниченийнаграницахполученныхразработаноавтоматическогоструктурныхисоискателемрезультатоввнедренопрограммноевыводагеометрическихкомпонентов.Полученныерезультаты были использованы на предприятии АО «Интел А/О» при8разработкемаршрутафизическогопроектированиябиблиотекстандартных ячеек.Достоверность полученных результатов и выводов подтвержденасогласованностью полученных в ходе экспериментальной проверкирезультатов,полученныхполученнымиприрекомендованныхвработе;положительнымисоответствующихВАКдляпубликацияхпубликациирецензиями,восновныхжурналах,результатовдиссертации на соискание ученой степени кандидата наук; разработкойдействующегопрограммногообеспечения,подтвержденнойсоответствующим актом внедрения.Личный вклад соискателя состоит в непосредственном участии вовсех этапах исследования, а именно: анализ существующих проблемв области методов решения задач оптимизации больших размерности,в частности проблемы применимости декларативного программированияи формальных методов к их решению подобных задач, формулировка целии задач исследования, разработка средств и методов для достиженияпоставленной цели, разработка вычислительного комплекса, а такжеапробация и внедрение результатов.