Автоматическая проверка синтезируемости описаний аппаратуры
Алексей Алексеевич ШЕВЦОВ,
Ян Андреевич ЧУРКИН,
Рубен Артурович БУЧАЦКИЙ,
Александр Сергеевич КАМКИН,
Дмитрий Михайлович МЕЛЬНИК https://doi.org/10.15514/ISPRAS-2026-38(4)-19
Аннотация
Современное проектирование цифровых СБИС предполагает использование языков описания аппаратуры Verilog и SystemVerilog как для логического синтеза, так и для симуляции, однако не все конструкции этих языков синтезируемы, а множество поддерживаемых конструкций различается между инструментами синтеза. При этом инструменты синтеза не всегда диагностируют несинтезируемые конструкции и могут молча изменять семантику схемы, что приводит к расхождению поведения RTL-модели и синтезированной схемы, а исправление проблем, обнаруженных на поздних этапах маршрута проектирования, требует значительных временных и экономических затрат. В работе описано формирование набора правил синтезируемости для описаний аппаратуры на языках Verilog и SystemVerilog на основе стандарта IEEE/IEC 62142-2005, руководства STARC RTL Design Style Guide и Reuse Methodology Manual, а также опыта коммерческих инструментов: сформулировано 34 правила, охватывающих не используемые при синтезе конструкции, семантику описаний аппаратных элементов и расхождение синтеза и симуляции. В рамках системы статического анализа SVAN реализованы статические детекторы для проверки соответствия исходного кода этим правилам: разработано 10 новых детекторов (SYNTH14–SYNTH23), обновлен 1 существующий (SYNTH13), часть правил покрывается ранее реализованными детекторами системы. Предложен механизм настройки уровня консервативности, позволяющий адаптировать строгость проверок к возможностям конкретного инструмента синтеза, в том числе с применением анализа потока данных; получены рекомендуемые конфигурации детекторов для инструментов синтеза Yosys, Vivado и Genus. Апробация на открытом инструменте Yosys показала, что несинтезируемые конструкции могут обрабатываться им без предупреждений с изменением семантики схемы, что подтверждает практическую значимость раннего статического анализа. Сравнение с коммерческим анализатором SpyGlass выявило конкретные пробелы в его анализе; нарушения правил найдены во всех десяти открытых проектах, на которых запускались детекторы, об одном из нарушений сообщено разработчикам проекта OpenC910.
Ключевые слова
статический анализ,
синтезируемость,
логический синтез,
язык описания и верификации аппаратуры SystemVerilog,
язык описания аппаратуры Verilog,
язык описания аппаратуры,
язык передачи регистров RTL,
сверхбольшие интегральные схемы СБИС,
системы автоматизации проектирования САПР,
синтез соединений Yosys
Об авторах
Алексей Алексеевич ШЕВЦОВ
Московский государственный университет имени М.В. Ломоносова
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Старший лаборант отдела компиляторных технологий ИСП РАН, студент ВМК МГУ имени М.В. Ломоносова. Научные интересы: статический анализ программ, языки описания аппаратуры, компиляторные технологии.
Ян Андреевич ЧУРКИН
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Научный сотрудник отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации, языки описания аппаратуры.
Рубен Артурович БУЧАЦКИЙ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Кандидат технических наук, старший научный сотрудник отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации.
Александр Сергеевич КАМКИН
Московский государственный университет имени М.В. Ломоносова
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Кандидат физико-математических наук, ведущий научный сотрудник отдела технологий программирования ИСП РАН. Научные интересы: формальные методы, синтез и верификация цифровой аппаратуры, гетерогенные компьютерные системы.
Дмитрий Михайлович МЕЛЬНИК
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Старший научный сотрудник отдела компиляторных технологий ИСП РАН. Научные интересы: компиляторные технологии, оптимизации.
Список литературы
1. IEEE Standard for Verilog Hardware Description Language. IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001), 2006, pp. 1-590. DOI: 10.1109/IEEESTD.2006.99495.
2. IEEE Standard for SystemVerilog – Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2023 (Revision of IEEE Std 1800-2017), 2024, pp. 1-1354. DOI: 10.1109/IEEESTD.2024.10458102.
3. IEEE Standard for Verilog Register Transfer Level Synthesis. IEC 62142:2005 / IEEE Std 1364.1-2002, 2005. 116 p.
4. RTL Design Style Guide for Verilog HDL. Semiconductor Technology Academic Research Center (STARC).
5. Keating M., Bricaud P. Reuse Methodology Manual for System-on-a-Chip Designs. Springer, 2002.
6. Yosys Open SYnthesis Suite. Available at: https://yosyshq.readthedocs.io/projects/yosys/en/latest/, accessed 01.06.2026.
7. Чуркин Я.А., Бучацкий Р.А., Китаев К.Н., Волохов А.Г., Долгодворов Е.В., Камкин А.С., Коцыняк А.М., Самоваров Д.О. Система статического анализа для языка описания аппаратуры SystemVerilog. Труды ИСП РАН, 2025, том 37, вып. 1, стр. 7-40. DOI: 10.15514/ISPRAS-2025-37(1)-1. / Churkin Ya.A., Buchatskiy R.A., Kitaev K.N., Volokhov A.G., Dolgodvorov E.V., Kamkin A.S., Kotsynyak A.M., Samovarov D.O. System for Static Analysis of SystemVerilog HDL. Trudy ISP RAN/Proc. ISP RAS, 2025, vol. 37, issue 1, pp. 7-40 (in Russian). DOI: 10.15514/ISPRAS-2025-37(1) 1.
8. Verible – SystemVerilog parser, linter, and formatter. Available at: https://github.com/chipsalliance/verible, accessed 01.06.2026.
9. svlint – SystemVerilog linter. Available at: https://github.com/dalance/svlint, accessed 01.06.2026.
10. Popoloski M. slang – SystemVerilog Language Services. Available at: https://github.com/MikePopoloski/slang, accessed 01.06.2026.
11. SpyGlass: Early Design Analysis Tools for SoCs. Available at: https://www.synopsys.com/verification/static-and-formal-verification/spyglass.html, accessed 01.06.2026.
12. Meredith P., Katelman M., Meseguer J., Roşu G. A Formal Executable Semantics of Verilog. In Proc. of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2010, pp. 179-188. DOI: 10.1109/MEMCOD.2010.5558634.
13. Lööw A. The Simulation Semantics of Synthesisable Verilog. Proceedings of the ACM on Programming Languages, 2025. DOI: 10.1145/3720484.
14. Lööw A. Lutsig: A Verified Verilog Compiler for Verified Circuit Development. In Proc. of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021. DOI: 10.1145/3437992.3439916.
15. Herklotz Y., Wickerson J. Finding and Understanding Bugs in FPGA Synthesis Tools. In Proc. of the 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, 2020. DOI: 10.1145/3373087.3375310.
16. ALINT-PRO. Available at: https://www.aldec.com/en/products/functional_verification/alint-pro, accessed 01.06.2026.
17. AMD Vivado Design Suite. Available at: https://www.amd.com/en/products/software/adaptive-socs-and-fpgas/vivado.html, accessed 01.06.2026.
18. Genus Synthesis Solution. Cadence Design Systems. Available at: https://www.cadence.com/en_US/home/tools/digital-design-and-signoff/synthesis/genus-synthesis-solution.html, accessed 01.06.2026.
19. Sutherland S., Mills D. Verilog and SystemVerilog Gotchas: 101 Common Coding Errors and How to Avoid Them. Springer, 2010. 218 p.
20. AES – Hardware implementation of AES encryption algorithm. Available at: https://github.com/secworks/aes, accessed 01.06.2026.
21. OpenXuantie – OpenC910 Core. Available at: https://github.com/XUANTIE-RV/openc910, accessed 01.06.2026.
22. CVA6 – an application class 6-stage RISC-V CPU. Available at: https://github.com/openhwgroup/cva6, accessed 01.06.2026.
23. Ibex – a small 32-bit RISC-V CPU core. Available at: https://github.com/lowRISC/ibex, accessed 01.06.2026.
24. OpenTitan – open source silicon root of trust. Available at: https://opentitan.org/, accessed 01.06.2026.
25. PicoRV32 – a size-optimized RISC-V CPU. Available at: https://github.com/YosysHQ/picorv32, accessed 01.06.2026.
26. VeeR EH1 Core. Available at: https://github.com/chipsalliance/Cores-VeeR-EH1, accessed 01.06.2026.
27. VeeR EL2 Core. Available at: https://github.com/chipsalliance/Cores-VeeR-EL2, accessed 01.06.2026.
28. SCR1 – an open-source RISC-V MCU core. Available at: https://github.com/syntacore/scr1, accessed 01.06.2026.
29. BlackParrot – a Linux-capable RISC-V multicore. Available at: https://github.com/black-parrot/black-parrot, accessed 01.06.2026.
30. OpenC910, GitHub issue #52. Available at: https://github.com/XUANTIE-RV/openc910/issues/52, accessed 01.06.2026.
Рецензия
Для цитирования:
ШЕВЦОВ А.А., ЧУРКИН Я.А., БУЧАЦКИЙ Р.А., КАМКИН А.С., МЕЛЬНИК Д.М. Автоматическая проверка синтезируемости описаний аппаратуры. Труды Института системного программирования РАН. 2026;38(4):45-66. https://doi.org/10.15514/ISPRAS-2026-38(4)-19
For citation:
SHEVTSOV A.A., CHURKIN Ya.A., BUCHATSKIY R.A., KAMKIN A.S., MELNIK D.M. Automatic Synthesizability Checking of Hardware Descriptions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2026;38(4):45-66. https://doi.org/10.15514/ISPRAS-2026-38(4)-19
Послать статью по эл. почте 