Применение инструмента SVAN статического анализа описаний аппаратуры для верификации открытых тестовых наборов
https://doi.org/10.15514/ISPRAS-2025-37(5)-10
Аннотация
В статье представлены результаты экспериментального анализа инструмента SVAN статического анализа описаний цифровой аппаратуры на языках Verilog и SystemVerilog. Инструмент разрабатывается в ИСП РАН и предоставляет средства формального и эвристического анализа HDL-описаний, нацеленные на выявление синтаксических ошибок, нарушений стиля оформления кода, проблем безопасности. Эксперименты, проведенные на описаниях из открытого тестового набора hdl-benchmarks, демонстрируют более высокую эффективность SVAN в сравнении с открытым инструментом Verilator и проприетарным инструментом Synopsys VCS. В частности, SVAN обнаружил на 73% больше типов ошибок и на 23-25% больше ошибок в целом. Ключевые преимущества инструмента SVAN состоят в более высоком уровне локализации ошибок и развитой типологии ошибок. К выявленным недостаткам инструмента SVAN относится ограниченная поддержка RTL-моделей, в которых используется несколько языков описания. Полученные результаты подчеркивают потенциал SVAN как конкурентоспособного инструмента статического анализа в области автоматизации проектирования цифровой аппаратуры.
Ключевые слова
статический анализ,
RTL-модель,
HDL-описание,
анализатор SVAN,
языки описания аппаратуры Verilog, SystemVerilog,
функциональная верификация,
обнаружение ошибок,
открытый тестовый набор.
При поддержке: Проект финансируется Министерством промышленности и торговли Российской Федерации в рамках ОКР «Разработка системы статического анализа для языка описания аппаратуры», шифр «САПР-Анализ» (в составе ОКР «САПР микроэлектроника», головной исполнитель – АО «МНТЦ МИЭТ»).
Об авторах
София Максимовна ПАНОВА
Институт системного программирования им. В.П. Иванникова РАН,
Российский экономический университет им. Г.В. Плеханова
Россия
Россия
Является лаборантом-исследователем отдела Технологий Программирования Института системного программирования им. В.П. Иванникова Российской академии наук (ИСП РАН). Область научных интересов: цифровая аппаратура, статический анализ, функциональная верификация.
Сергей Александрович СМОЛОВ
Институт системного программирования им. В.П. Иванникова РАН,
Российский экономический университет им. Г.В. Плеханова
Россия
Россия
Является научным сотрудником отдела Технологий Программирования Института системного программирования им. В.П. Иванникова Российской академии наук (ИСП РАН), старший научный сотрудник научной лаборатории «Гетерогенные компьютерные системы» РЭУ им. Г.В. Плеханова. Область научных интересов: автоматизация проектирования цифровой аппаратуры, верификация и тестирование.
Марина М. ВОЛКОВА
Институт системного программирования им. В.П. Иванникова РАН,
Российский экономический университет им. Г.В. Плеханова
Россия
Россия
Является лаборантом отдела Технологий Программирования Института системного программирования им. В.П. Иванникова Российской академии наук (ИСП РАН). Область научных интересов: машинное обучение, интеллектуальный анализ данных, методы статического анализа и верификации.
Список литературы
1. IEEE SA. IEEE Standard for Verilog Hardware Description Language [Online]. Available: https://standards.ieee.org/ieee/1364/3641/ (accessed 2025, Mar. 27).
2. IEEE SA. IEEE Standard for SystemVerilog – Unified Hardware Design, Specification, and Verification Language [Online]. Available: https://standards.ieee.org/ieee/1800/7743/ (accessed 2025, Mar. 27).
3. NVDLA Project, “NVIDIA Deep Learning Accelerator (NVDLA) – Open-Source Inference Accelerator”, GitHub repository, 2017-2023. [Online]. Available: https://github.com/nvdla (accessed 2025, Mar. 27).
4. GOST R 71207-2024, “Information Protection. Secure Software Development. Static Code Analysis. General Requirements”, Moscow: Standartinform, 2024. [Online]. Available: https://protect.gost.ru/v.aspx?control=7&id=257752 (accessed 2025, Mar. 27).
5. Synopsys, “VCS® Functional Verification Solution”, Synopsys Inc., 2023. [Online]. Available: https://www.synopsys.com/verification/simulation/vcs.html (accessed 2025, Mar. 27).
6. Synopsys, “SpyGlass: Early Design Analysis Tools for SoCs”, Synopsys Inc., 2025. [Online]. Available: https://www.synopsys.com/verification/static-and-formal-verification/spyglass.html (accessed 2025, Jun.12).
7. Cadence Design Systems, “Formal and Static Verification Solutions”, Cadence Inc., 2023. [Online]. Available: https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification.html (accessed 2025, Mar. 27).
8. Siemens EDA (2025, Mar. 27). Questa Verification Solutions, Siemens Digital Industries Software, 2023. [Online]. Available: https://eda.sw.siemens.com/en-US/ic/questa/ (accessed 2025, Mar. 27).
9. M. Popoloski, slang: SystemVerilog Language Services, version 8.0, 2015-2025. [Online]. Available: https://github.com/MikePopoloski/slang (accessed 2025, Mar. 27).
10. Verilator. Verilator – a fast Verilog/SystemVerilog simulator. GitHub repository, 2003-2024. [Online]. Available: https://github.com/verilator/verilator (accessed 2025, Mar. 27).
11. D. Alance. svlint – SystemVerilog linter. GitHub repository 2020-2024. (2025, Mar. 27). [Online]. Available: https://github.com/dalance/svlint (accessed 2025, Mar. 27).
12. CHIPS Alliance, Surelog v1.84 – SystemVerilog 2017 Toolchain, 2024. [Online]. Available: https://github.com/chipsalliance/Surelog (accessed 2025, Mar. 27).
13. CHIPS Alliance. Verible – Suite of SystemVerilog developer tools. GitHub repository, 2019-2024. [Online]. Available: https://github.com/chipsalliance/verible (accessed 2025, Mar. 27).
14. T. Pecenka, L. Sekanina, and Z. Kotasek, “Evolution of synthetic RTL benchmark circuits with predefined testability”, ACM Trans. Des. Autom. Electron. Syst., vol. 13, no. 3, pp. 1–21, Jul. 2008.
15. F. Yuan, “Design and Test for Timing Uncertainty in VLSI Circuits”, Ph.D. dissertation, Chinese University of Hong Kong, Hong Kong, 2012.
16. Ya. A. Churkin, R. A. Buchatskiy, K. N. Kitaev, A. G. Volokhov, E. V. Dolgodvorov, A. S. Kamkin, A. M. Kotsynyak, and D. O. Samovarov, “Static Analysis System for SystemVerilog Hardware Description Language”, Proceedings of the ISP RAS, vol. 37, no. 1, pp. 7–40, 2025.
17. International Workshop on Logic & Synthesis (IWLS), “IWLS 2005 Benchmark Suite”, 2005. [Online]. Available: https://iwls.org/iwls2005/benchmarks.html (accessed 2025, Mar. 27).
18. N. Isaac, “QUIP Toolkit Benchmarks (v9.0)”, ECE496 GitHub repository, 2020. [Online]. Available: https://github.com/neilisaac/ece496/tree/master/reference/quip_toolkit-9.0/benchmarks (accessed 2025, Mar. 27).
19. hdl-benchmarks – Collection of digital hardware modules & projects (benchmarks), GitHub repository, 2019-2023. [Online]. Available: https://github.com/ispras/hdl-benchmarks (accessed 2025, Apr. 06).
20. Freescale Semiconductor, Verilog HDL Coding: Semiconductor Reuse Standard. Freescale Semiconductor, Inc., 2005.
21. M. Taylor and Bespoke Silicon Group. BSG SystemVerilog Coding Standards, University of Washington, 2023.
22. C. Wolf, “PicoRV32 – A Size-Optimized RISC-V CPU Core”, YosysHQ GitHub repository, 2015-2023. [Online]. Available: https://github.com/YosysHQ/picorv32 (accessed 2025, Mar. 27).
23. OpenHW Group, “CVA6 – An Open-Source 64-bit RISC-V CPU Core”, GitHub repository, 2019-2023. [Online]. Available: https://github.com/openhwgroup/cva6 (accessed 2025, Mar. 27).
24. lowRISC, “OpenTitan – Open Source Silicon Root of Trust”, GitHub repository, 2018-2023. [Online]. Available: https://github.com/lowRISC/opentitan (accessed 2025, Mar. 27).
25. M. Hansen, H. Yalcin, J. Hayes, “Unveiling the ISCAS-85 benchmarks: A case study in reverse engineering”, IEEE Design & Test of Computers, vol. 16, no. 3, pp. 72-80, 1999.
26. F. Brglez, D. Bryan, K. Kozminski, “Combinational Profiles of Sequential Benchmark Circuits”, Proc. IEEE Int. Symposium on Circuits and Systems, pp. 1929-1934, May 1989.
27. Microelectronics Center in North Carolina. LGSynth91 benchmarks. [Online]. Available: https://ddd.fit.cvut.cz/www/prj/Benchmarks/LGSynth91.7z (accessed 2025, Jun. 14).
28. Department of Electrical and Computer Engineering at the University of Texas. Texas-97 benchmarks. [Online]. Available: https://ptolemy.berkeley.edu/projects/embedded/research/vis/texas-97 (accessed 2025, Jun. 14).
29. University of Oxford. VCEGAR benchmarks. [Online]. Available: http://www.cprover.org/hardware/benchmarks/vcegar-benchmarks.tgz (accessed 2025, Jun. 14).
30. FBK, “Verilog2SMV”, Fondazione Bruno Kessler (FBK). [Online]. Available: https://es- static.fbk.eu/tools/verilog2smv/ (accessed 2025, Mar. 29).
Рецензия
Для цитирования:
ПАНОВА С.М., СМОЛОВ С.А., ВОЛКОВА М.М. Применение инструмента SVAN статического анализа описаний аппаратуры для верификации открытых тестовых наборов. Труды Института системного программирования РАН. 2025;37(5):131-142. https://doi.org/10.15514/ISPRAS-2025-37(5)-10
For citation:
PANOVA S.M., SMOLOV S.A., VOLKOVA M.М. Application of SVAN Static Analysis Tool on Open RTL Benchmarks. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(5):131-142. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(5)-10
Послать статью по эл. почте 