Система статического анализа для языка описания аппаратуры SystemVerilog
Ян Андреевич ЧУРКИН,
Рубен Артурович БУЧАЦКИЙ,
Константин Николаевич КИТАЕВ,
Алексей Георгиевич ВОЛОХОВ,
Егор Викторович ДОЛГОДВОРОВ,
Александр Сергеевич КАМКИН,
Артем Михайлович КОЦЫНЯК,
Дмитрий Олегович САМОВАРОВ https://doi.org/10.15514/ISPRAS-2025-37(1)-1
Аннотация
Рост сложности современных цифровых систем и увеличение объемов кода на языках описания аппаратуры требуют эффективных инструментов для выявления ошибок на ранних этапах разработки цифровых СБИС. Для своевременного обнаружения ошибок составляются сборники правил, регламентирующие описание аппаратуры. Эти сборники содержат набор правил, описывающих неточности, ошибки и последствия их нарушения. В данной работе рассмотрен список правил, разработанный на основе опыта работы инженеров, использующих язык SystemVerilog, и представлена система статического анализа SVAN, разработанная для языка SystemVerilog и учитывающая специфику описаний аппаратуры. Предлагаемая система обеспечивает полную поддержку стандарта SystemVerilog IEEE 1800-2017 и предоставляет возможности анализа описаний на наличие структурных и семантических ошибок.
Ключевые слова
статический анализ,
язык описания аппаратуры,
язык описания аппаратуры Verilog,
язык описания аппаратуры SystemVerilog,
интегральная схема,
система автоматизации проектирования (САПР),
инструментарий анализа, компиляции и выполнения описаний аппаратуры slang, slang-tidy, KLEE, Yosys, Verilator, CIRCT,
проект LLVM,
абстрактное синтаксическое дерево АСД.
При поддержке: Проект финансируется Минпромторгом России в рамках ОКР «Разработка системы статического анализа для языка описания аппаратуры», шифр «САПР-Анализ» (в составе ОКР «САПР микроэлектроника», головной исполнитель – АО «МНТЦ МИЭТ»).
Об авторах
Ян Андреевич ЧУРКИН
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Младший научный сотрудник отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации, языки описания аппаратуры.
Рубен Артурович БУЧАЦКИЙ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Кандидат технических наук, научный сотрудник отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации.
Константин Николаевич КИТАЕВ
Институт системного программирования им. В.П. Иванникова РАН,
Московский физико-технический институт
Россия
Россия
Студент МФТИ, лаборант отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации.
Алексей Георгиевич ВОЛОХОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Ведущий инженер отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации.
Егор Викторович ДОЛГОДВОРОВ
Московский физико-технический институт
Россия
Россия
Студент МФТИ, Научные интересы: статический анализ программ, компиляторные технологии, оптимизации.
Александр Сергеевич КАМКИН
Институт системного программирования им. В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова, Московский физико-технический институт, Российский экономический университет имени Г.В. Плеханова
Россия
Россия
Кандидат физико-математических наук, ведущий научный сотрудник отдела технологий программирования ИСП РАН, ведущий научный сотрудник РЭУ им. Г.В. Плеханова. Научные интересы: формальные методы, синтез и верификация цифровой аппаратуры, гетерогенные компьютерные системы.
Артем Михайлович КОЦЫНЯК
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Научный сотрудник отдела технологий программирования ИСП РАН. Научные интересы: формальные методы, компиляторные технологии, модели вычислений, языки программирования.
Дмитрий Олегович САМОВАРОВ
Институт системного программирования им. В.П. Иванникова РАН, Московский государственный университет имени М.В. Ломоносова
Россия
Россия
Стажер-исследователь отдела компиляторных технологий ИСП РАН. Научные интересы: статический анализ программ, компиляторные технологии, оптимизации, языки описания аппаратуры.
Список литературы
1. Riesgo T., Torroja Y., de la Torre E. Design Methodologies Based on Hardware Description Languages. IEEE Transactions on Industrial Electronics, vol. 46, no. 1, 1999. pp. 3-12. DOI: 10.1109/41.744370.
2. Earlham College. – Intel Pentium fdiv error, https://www.cs.earlham.edu/~dusko/cs63/fdiv.html, accessed 01.12.2024
3. Mcilroy R., Sevcik J., Tebbi T., Titzer B.L., Verwaest T. Spectre is here to stay: An analysis of side-channels and speculative execution. arXiv:1902.05178, 2019. https://arxiv.org/abs/1902.05178.
4. IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2017. 1315 p. DOI: 10.1109/IEEESTD.2018.8299595.
5. IEEE Standard for VHDL Language Reference Manual. IEEE Std 1076-2019. 673 p. DOI: 10.1109/IEEESTD.2019.8938196.
6. Смолов С.А. Обзор методов извлечения моделей из HDL-описаний. Труды ИСП РАН, том 27, вып. 1, 2015. с. 97-124. DOI: 10.15514/ISPRAS-2015-27(1)-6.
7. "IEEE Standard for Verilog Hardware Description Language," in IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001), vol., no., pp.1-590, 7 April 2006, doi: 10.1109/IEEESTD.2006.99495.
8. EBMC – model checker for hardware designs, accessed 12.04.2024. https://www.cprover.org/ebmc, accessed 01.12.2024
9. Zhang R., Deutschbein C., Huang P., Sturton C. End-to-End Automated Exploit Generation for Validating the Security of Processor Designs. IEEE/ACM International Symposium on Microarchitecture (MICRO), 2018. pp. 815-827. DOI: 10.1109/MICRO.2018.00071.
10. sv-tests – SystemVerilog parsing synthetic test suit. https://github.com/chipsalliance/sv-tests, accessed 01.12.2024
11. SpyGlass: Early Design Analysis Tools for SoCs.
12. https://www.synopsys.com/verification/static-and-formal-verification/spyglass.html, accessed 01.12.2024
13. VCS: Functional Verification Solution. https://www.synopsys.com/verification/simulation/vcs.html, accessed 01.12.2024
14. IEEE Standard for Universal Verification Methodology Language Reference Manual. IEEE Std 1800.2-2020. 458 p. DOI: 10.1109/IEEESTD.2020.9195920.
15. Jasper Formal Verification Platform.
16. https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification.html, accessed 01.12.2024
17. Xcelium logic simulation.
18. https://www.cadence.com/en_US/home/tools/system-design-and-verification/simulation-and-testbench-verification/xcelium-simulator.html, accessed 01.12.2024
19. Claire Wolf. Yosys Open SYnthesis Suite. https://yosyshq.net/yosys/, accessed 01.12.2024
20. Icarus Verilog, https://steveicarus.github.io/iverilog/, accessed 01.12.2024
21. Verible – SystemVerilog parser and linter, https://github.com/chipsalliance/verible, accessed 01.12.2024
22. svlint – SystemVerilog linter, https://github.com/dalance/svlint, accessed 01.12.2024
23. SystemVerilog parser library, https://github.com/dalance/sv-parser, accessed 01.12.2024
24. Verilator – SystemVerilog simulation tool, https://github.com/verilator/verilator, accessed 01.12.2024
25. KLEE – symbolic virtual machine built on top of the LLVM compiler infrastructure, https://github.com/klee, accessed 01.12.2024
26. Surelog – SystemVerilog 2017 pre-processor, parser, elaborator, UHDM compiler, https://github.com/chipsalliance/Surelog, accessed 01.12.2024
27. Dargelas A., Zeller H. Universal Hardware Data Model. Workshop on Open-Source EDA Technology (WOSET), 2020. https://woset-workshop.github.io/PDFs/2020/a10.pdf
28. CIRCT – Circuit IR Compilers and Tools, https://github.com/llvm/circt, accessed 01.12.2024
29. Lattner C. et al. MLIR: A compiler infrastructure for the end of Moore's law // arXiv preprint arXiv:2002.11054. – 2020.
30. Mike Popoloski, slang - SystemVerilog Language Services, https://github.com/MikePopoloski/slang, accessed 01.12.2024
31. Mike Popoloski, slang-tidy - SystemVerilog linter,
32. https://github.com/MikePopoloski/slang/tree/master/tools/tidy, accessed 01.12.2024
33. slang based frontend for Yosys, https://github.com/povik/yosys-slang, accessed 01.12.2024
34. Takemoto T. Joint activity for semiconductor R&D and role of Semiconductor Technology Academic Research Center (STARC). International Symposium on VLSI Technology, Systems, and Applications, 2001. pp. 7-10. DOI: 10.1109/VTSA.2001.934468.
35. Synopsis Inc., Mentor Graphics Corporation (2001). OpenMORE Assessment Program for Hard/Soft IP Version 1.0, http://www.openmore.com, accessed 01.12.2024
36. Hilderman V., Baghi T. Avionics Certification: A Complete Guide to DO-178 (Software), DO-254 (Hardware). Avionics Communications, 2007. 244 p.
37. Clang: a C language family frontend for LLVM, https://clang.llvm.org, accessed 01.12.2024
38. LLVM Language Reference Manual, https://llvm.org/docs/LangRef.html, accessed 01.12.2024
39. Moore Dialect, https://circt.llvm.org/docs/Dialects/Moore/, accessed 01.12.2024
40. Erhart M., Schuiki F., Yedidia Z., Healy B., Grosser T. Arcilator: Fast and cycle-accurate hardware simulation in CIRCT. LLVM Developers Meeting, 2023.
41. https://llvm.org/devmtg/2023-10/slides/techtalks/Erhart-Arcilator-FastAndCycleAccurateHardwareSimulationInCIRCT.pdf
42. The RTL Intermediate Language (RTLIL),
43. https://yosyshq.readthedocs.io/projects/yosys/en/stable/yosys_internals/formats/rtlil_rep.html, accessed 01.12.2024
44. Sutherland S., Mills D. Verilog and SystemVerilog Gotchas: 101 Common Coding Errors and How to Avoid Them. Springer, 2010. 218 p.
45. AES – Hardware implementation of AES encryption algorithm, https://github.com/secworks/aes, accessed 01.12.2024
46. PicoRV32 – A Size-Optimized RISC-V CPU, https://github.com/YosysHQ/picorv32, accessed 01.12.2024
47. Black Parrot – A Linux-Capable Accelerator Host RISC-V Multicore,
48. https://github.com/black-parrot/black-parrot, accessed 01.12.2024
49. The CORE-V CVA6 is an Application class 6-stage RISC-V CPU capable of booting Linux, https://github.com/openhwgroup/cva6, accessed 01.12.2024
50. SCR1 – RISC-V Core, accessed 10.06.2024. https://github.com/syntacore/scr1, accessed 01.12.2024
51. Ibex – RISC V Core, https://github.com/lowRISC/ibex, accessed 01.12.2024
52. VeeR EH1 Core, https://github.com/chipsalliance/Cores-VeeR-EH1, accessed 01.12.2024
53. OpenXuantie – OpenC910 Core, https://github.com/XUANTIE-RV/openc910, accessed 01.12.2024
54. ASIC Design for Bitcoin Mining, https://github.com/susansun1999/eecs570_final_project, accessed 01.12.2024
55. Sun Y., Yang H., Zhang W., Gu Y. ASIC Design for Bitcoin Mining. University of Michigan, 2021.
56. https://zwtaoumich.github.io/paper/EECS570_Final_Report.pdf
57. OpenTitan: Open source silicon root of trust (RoT). https://opentitan.org/, accessed 01.12.2024
58. black-parrot, Hotfix: orbc typo,
59. https://github.com/black-parrot/black-parrot/pull/1228/commits/87866ddfa37ab9d5df8e5951d3b7865b23676c77, accessed 01.12.2024
60. Case label selector mismatch. https://github.com/black-parrot/black-parrot/issues/1230, accessed 01.12.2024
61. Fix case label mismatch. https://github.com/black-parrot/black-parrot/pull/1232, accessed 01.12.2024
62. RISC-V Platform-Level Interrupt Controller. https://github.com/pulp-platform/rv_plic/, accessed 01.12.2024
63. Adjust codegen to fix synthesis latch. https://github.com/pulp-platform/rv_plic/pull/7, accessed 01.12.2024
Рецензия
Для цитирования:
ЧУРКИН Я.А., БУЧАЦКИЙ Р.А., КИТАЕВ К.Н., ВОЛОХОВ А.Г., ДОЛГОДВОРОВ Е.В., КАМКИН А.С., КОЦЫНЯК А.М., САМОВАРОВ Д.О. Система статического анализа для языка описания аппаратуры SystemVerilog. Труды Института системного программирования РАН. 2025;37(1):7-40. https://doi.org/10.15514/ISPRAS-2025-37(1)-1
For citation:
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. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(1):7-40. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(1)-1
Послать статью по эл. почте 