Заведующий лабораторией: к.ф.-м.н. Александр Сергеевич Камкин
Число сотрудников: около 50 человек
Проектирование цифровых устройств (процессоров, контроллеров, специализированных вычислителей и др.) — сложный процесс, который включает разработку исходного кода на Verilog/SystemVerilog/VHDL, синтез логической схемы, генерацию топологии микросхемы и верификацию. Для реализации данного процесса используются системы автоматизации проектирования (САПР). Разработкой таких систем и занимается команда Лаборатории технологий проектирования цифровой аппаратуры. Лаборатория входит в состав Отдела технологий программирования ИСП РАН.
| Направления | Задачи |
|---|---|
| Логический синтез | |
| Трансляция HDL-описаний и конструирование логических схем | Как построить схему из логических вентилей по высокоуровневому описанию? |
| Технологически независимая оптимизация | Как минимизировать число логических вентилей в схеме и/или её глубину? |
| Технологическое отображение | Как выразить схему в терминах технологических ячеек? Можно ли улучшить схему, синтезированную для конкретной фабрики? |
| Проверка корректности (верификация) | |
| Проверка логической эквивалентности | Как проверить, что разные схемы на одинаковых данных всегда возвращают один и тот же результат? А если в схемах есть память? А если в схемах миллион элементов? |
| Функциональная верификация | Как эффективно искать ошибки в микропроцессорах ARM или RISC-V? А если это процессор с новой архитектурой? |
| Статический анализ | Как научить программу искать ошибки в аппаратуре? А если описание аппаратуры состоит из сотен миллионов строк на языке SystemVerilog? |
| Машинное обучение в САПР | |
| Прогнозирование | Можно ли предсказать результат синтеза заранее? |
| Логическая оптимизация | Можем ли мы научить нейросеть оптимизировать схемы? Можно ли из RL-агента сделать тополога? |
| Генерация описаний аппаратуры | Снятся ли нейросетям микропроцессоры? |
| Высокоуровневый синтез | |
| Синтез потоковых вычислителей | Как разработать процессор на C++? Можно ли его сделать самым быстрым в мире и изготовить на фабрике? |
| Поддержка процессов разработки | |
| Тестирование | Как помочь команде, занимающейся разработкой промышленной САПР из большого числа компонентов? Как разработать набор тестовых примеров, который будут использовать ученые и инженеры во всем мире? |
Стек технологий
Языки разработки — C/C++, Python, Java
Языки проектирования — Verilog, SystemVerilog, VHDL
Сборка — CMake
DevOps — Docker, GitLab CI/CD (YAML)
Управление разработкой — Git, GitLab, Jira/Confluence/Nextcloud
ОС — Linux
Используемые открытые решения — Yosys, OpenLane, Slang
Наши открытые проекты
- Utopia EDA (https://gitlab.ispras.ru/mvg/utopia-eda) — среда синтеза логических схем по описаниям аппаратуры на языках Verilog и SystemVerilog
- Utopia HLS (https://github.com/ispras/utopia-hls) — инструмент высокоуровневого синтеза описаний цифровой аппаратуры
- MicroTESK (http://www.microtesk.org) — среда разработки генераторов тестовых программ для микропроцессоров
- Retrascope (https://forge.ispras.ru/projects/retrascope) — инструмент обратной инженерии и формальной верификации на модульном уровне
- C++TESK (https://forge.ispras.ru/projects/cpptesk-toolkit) — инструмент имитационной верификации Verilog-описаний
Наши ключевые публикации
- Система статического анализа для языка описания аппаратуры SystemVerilog. Я.А. Чуркин, Р.А. Бучацкий, К.Н. Китаев, А.Г. Волохов, Е.В. Долгодворов, А.С. Камкин, А.М. Коцыняк, Д.О. Самоваров, 2025.
https://ispranproceedings.elpub.ru/jour/article/download/1886/1739 - Предсказание характеристик СБИС по логической схеме с помощью методов машинного обучения. М.С. Лебедев, Д.А. Дыскина, А.Ю. Еременко, Ф.А. Кабанов, И.А. Козмин, Д.М. Петренко, Н.Б. Поудиал, А.А. Сергеев, Р.А. Ширинова, 2025. https://www.mathnet.ru/php/getFT.phtml?jrnid=tisp&paperid=965&what=fullt&option_lang=eng
- Experimental Comparison of Logic Circuit Synthesis Methods. M.D. Vershkov, A.A. Yagzhov, N.S. Romanov, A.A. Fedotova, E.P. Znatnov, 2024. http://syrcose.ispras.ru/2024/submissions/SYRCoSE_2024_paper_09_7.pdf
- High-Level Synthesis versus Hardware Construction. A. Kamkin, M. Chupilko, M. Lebedev, S. Smolov, G. Gayadjiev, 2023.
https://research.rug.nl/files/916133599/High-Level_Synthesis_versus_Hardware_Construction.pdf - Сравнение открытых маршрутов проектирования цифровой аппаратуры: qFlow, OpenLANE, Coriolis, SymbiFlow. А.С. Камкин, С.А. Смолов, М.М. Чупилко, 2021. https://ispranproceedings.elpub.ru/jour/article/view/1475?locale=ru_RU
- A Survey of Open-source Tools for FPGA-based Inference of Artificial Neural Networks. M. Lebedev, P. Belecky, 2021.
https://www.researchgate.net/publication/358325908_A_Survey_of_Open-source_Tools_for_FPGA-based_Inference_of_Artificial_Neural_Networks - Retrascope: Open-Source Model Checker for HDL Descriptions. A. Kamkin, M. Lebedev, S. Smolov, 2019.
https://dvcon-proceedings.org/wp-content/uploads/Retrascope-Open-Source-Model-Checkerfor-HDL-Descriptions.pdf - MicroTESK: A Tool for Constrained Random Test Program Generation for Microprocessors. A. Kamkin, A. Tatarnikov, 2018.
https://link.springer.com/chapter/10.1007/978-3-319-74313-4_28 - Средства функциональной верификации микропроцессоров. А.С. Камкин, А.М. Коцыняк, С.А. Смолов, А.А. Сортов, А.Д. Татарников, М.М. Чупилко, 2014. https://ispranproceedings.elpub.ru/jour/article/view/771?locale=ru_RU
- Механизмы поддержки тестирования моделей аппаратуры на разных уровнях абстракции. А.С. Камкин, М.М. Чупилко, 2011.
https://ispranproceedings.elpub.ru/jour/article/view/1057?locale=ru_RU - Применение технологии UniTesK для функционального тестирования моделей аппаратного обеспечения. В.П. Иванников, А.С. Камкин, В.В. Кулямин, А.К. Петренко, 2006. https://citforum.ru/SE/testing/unitesk_hard/
Темы защищенных квалификационных работ
Примеры тем курсовых работ:
— Курганская А.С. Исследование и разработка методов оптимизации комбинационных логических схем с использованием обучения с подкреплением;
— Литвинов М.Ю. Разработка средств высокоуровневого синтеза и оптимизации потоковых вычислителей, реализующих алгоритмы блочного шифрования.
Примеры тем дипломных работ:
— Козмин И.А. Разработка модели автокодировщика логических схем;
— Ершов М.А. Исследование и разработка средств извлечения конечных автоматов из синхронных схем;
— Вершков М.Д. Разработка и исследование методов оптимизации аппаратных реализаций алгоритмов блочного шифрования на этапе логического синтеза.
Кандидатские диссертации:
— Татарников А.Д. Автоматизация конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций;
— Чупилко М.М. Метод автоматизации динамической верификации цифровой аппаратуры на основе формальных спецификаций разного уровня абстракции;
— Камкин А.С. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций.