Отримано 17.02.2026, Доопрацьовано 26.05.2026, Прийнято 25.06.2026 Опубліковано 03.08.2026

Методи функціональної та формальної верифікації цифрових систем: теоретичний аналіз та експериментальне застосування до модулів різної складності

Олександр Острянко*

oleksandrostrianko@outlook.com



Метою дослідження було теоретичне обґрунтування сутності функціональної та формальної верифікації цифрових систем, порівняння їхніх методів і визначення можливостей узгодженого застосування до цифрових модулів різної структурної складності. Методологія ґрунтувалася на нормативно-термінологічному, структурно-аналітичному, функціонально-верифікаційному, формально-логічному та порівняльноаналітичному методах, що дало змогу розмежувати сценарний і властивісний підходи до перевірки апаратної логіки та здійснити експериментально-демонстраційну перевірку трьох тестових цифрових модулів. Установлено, що функціональна верифікація забезпечувала перевірку поведінкової відповідності цифрового модуля специфікації через тестові впливи, очікувані вихідні реакції, тестбенчі, симуляцію та аналіз покриття функціональних режимів. Формальна верифікація формувала інший тип перевірочного висновку, оскільки була спрямована на підтвердження або спростування властивостей коректності, інваріантів, логічних і часових умов, допустимих переходів та недосяжності помилкових станів. Експериментально-демонстраційна перевірка на мультиплексорі, скінченному автоматі та спрощеному інтерфейсному контролері показала, що зі зростанням складності цифрового модуля збільшувалася кількість функціональних сценаріїв, ускладнювалося покриття режимів і зростав ризик невиявлення прихованих станів, блокувань або рідкісних комбінацій сигналів. Для мультиплексора обидва підходи дали узгоджений результат; для скінченного автомата зросло значення перевірки скидання, станів і переходів; для інтерфейсного контролера формальна перевірка посилила оцінку блокувань, конфліктів сигналів і помилкових режимів. Обґрунтовано доцільність комбінованої стратегії, у якій функціональні сценарії, аналіз покриття, формальні властивості та інтерпретація можливих контрприкладів взаємно доповнюють один одного. Практичне значення результатів полягає в їх використанні в цифровому проєктуванні, апаратній верифікації та навчально-дослідних середовищах для планування перевірки цифрових модулів, уточнення специфікацій, аналізу покриття, інтерпретації контрприкладів і прийняття рішення щодо коректності апаратної логіки

апаратна логіка; тестові сценарії; аналіз покриття; властивості коректності; контрприклади; керувальні сигнали
132-144
Ostrianko, O. (2026). Methods of functional and formal verification of digital systems: Theoretical analysis and experimental application to modules of varying complexity. Information Technologies and Computer Engineering, 23(2), 132-144. https://doi.org/10.31649/vitce/2.2026.132.

Використані джерела

  1. Abdollahi, M., Yeganeh, S.F., Baharloo, M.A., & Baniasadi, A. (2025). Hardware design and verification with large language models: A scoping review, challenges, and open issues. Electronics, 14(1), article number 120. doi: 10.3390/electronics14010120.
  2. Anwar, M.W., Rashid, M., Azam, F., Naeem, A., Kashif, M., & Butt, W.H. (2020). A unified model-based framework for the simplified execution of static and dynamic assertion-based verification. IEEE Access, 8, 104407-104431. doi: 10.1109/ACCESS.2020.2999544.
  3. Beyer, D., Chien, P.-C., Jankola, M., & Lee, N.-Z. (2024). A transferability study of interpolation-based hardware model checking for software verification. Proceedings of the ACM on Software Engineering, 1, article number 90. doi: 10.1145/3660797.
  4. Cabodi, G., Camurati, P.E., Palena, M., & Pasini, P. (2024). Hardware model checking algorithms and techniques. Algorithms, 17(6), article number 253. doi: 10.3390/a17060253.
  5. Chuah, C.S., Appold, C., & Leinmueller, T. (2023). Formal verification of security properties on RISC-V processors. In MEMOCODE ‘23: Proceedings of the 21st ACM-IEEE international conference on formal methods and models for system design (pp. 159-168). New York: Association for Computing Machinery. doi: 10.1145/3610579.3611085.
  6. Dobis, A., Laeufer, K., Damsgaard, H.J., Petersen, T., Rasmussen, K.J.H., Tolotto, E., Andersen, S.T., Lin, R., & Schoeberl, M. (2023). Verification of Chisel hardware designs with ChiselVerify. Microprocessors and Microsystems, 96, article number 104737. doi: 10.1016/j.micpro.2022.104737.
  7. Elakkiya, C., Murty, N.S., Babu, C., & Jalan, G. (2017). Functional coverage – driven UVM based JTAG verification. In 2017 IEEE international conference on computational intelligence and computing research (pp. 1-7). New York: IEEE. doi: 10.1109/ICCIC.2017.8524556.
  8. Farooq, U., & Mehrez, H. (2021). Pre-silicon verification using multi-FPGA platforms: A review. Journal of Electronic Testing, 37, 7-24. doi: 10.1007/s10836-021-05929-1.
  9. Georgoulopoulos, N., Mamali, T., & Hatzopoulos, A.A. (2024). Design and verification of a SAR ADC SystemVerilog real number model. Journal of Electronic Testing, 40, 315-328. doi: 10.1007/s10836-024-06124-8.
  10. Guzmán-Miranda, H., García, M.L., & Aguado, A.U. (2025). FVM: A formal verification methodology for VHDL designs. IEEE Open Journal of the Computer Society, 6, 1920-1933. doi: 10.1109/OJCS.2025.3625468.
  11. Hsiao, Y., Mulligan, D.P., Nikoleris, N., Petri, G., & Trippel, C. (2021). Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations. In MICRO-54: Proceedings of the 54th annual IEEE/ACM international symposium on microarchitecture (pp. 679-694). New York: Association for Computing Machinery. doi: 10.1145/3466752.3480087.
  12. IEEE 1012-2024. (2025). IEEE standard for system, software, and hardware verification and validation. Retrieved from https://standards.ieee.org/ieee/1012/7324/.
  13. IEEE 1076-2019. (2019). IEEE standard for VHDL language reference manual. Retrieved from https://standards.ieee.org/ieee/1076/5179/.
  14. IEEE 1800.2-2020. (2020). IEEE standard for Universal Verification Methodology language reference manual. Retrieved from https://standards.ieee.org/ieee/1800.2/7567.
  15. IEEE 1800-2023. (2024). IEEE standard for SystemVerilog – unified hardware design, specification, and verification language. Retrieved from https://standards.ieee.org/ieee/1800/7743.
  16. IEEE 1850-2010. (2010). IEEE standard for Property Specification Language (PSL). Retrieved from https://standards.ieee.org/ieee/1850/4383/.
  17. ISO/IEC/IEEE 24765:2017. (2017). Systems and software engineering – vocabulary. Retrieved from https://www.iso.org/standard/71952.html.
  18. ISO/IEC/IEEE 29119-1:2022. (2022). Software and systems engineering – software testing. Part 1: General concepts. Retrieved from https://www.iso.org/standard/81291.html.
  19. Karmakar, R. (2022). Formal verification techniques: A comparative analysis for critical system design. In A. Abraham, N. Gandhi, T. Hanne, T.-P. Hong, T.N. Rios & W. Ding (Eds.), 21st international conference on intelligent systems design and applications (ISDA 2021): Intelligent systems design and applications (pp. 93-102). Cham: Springer. doi: 10.1007/978-3-030-96308-8_9.
  20. Kern, C., & Greenstreet, M.R. (1999). Formal verification in hardware design: A survey. ACM Transactions on Design Automation of Electronic Systems, 4(2), 123-193. doi: 10.1145/307988.307989.
  21. Khan, W., Kamran, M., Naqvi, S.R., Khan, F.A., Alghamdi, A.S., & Alsolami, E. (2020). Formal verification of hardware components in critical systems. Wireless Communications and Mobile Computing, 2020(1), article number 7346763. doi: 10.1155/2020/7346763.
  22. Lai, X., Balakrishnan, A., Lange, T., Jenihhin, M., Ghasempouri, T., Raik, J., & Alexandrescu, D. (2019). Understanding multidimensional verification: Where functional meets non-functional. Microprocessors and Microsystems, 71, article number 102867. doi: 10.1016/j.micpro.2019.102867.
  23. Ma, R., Huang, J., Zhang, S., Xie, Y., & Luo, G. (2025). NoCFuzzer: Automating NoC verification in UVM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 44(1), 371-384. doi: 10.1109/TCAD.2024.3430195.
  24. Mehta, A.B. (2018). ASIC/SoC functional design verification: A comprehensive guide to technologies and methodologies. Cham: Springer. doi: 10.1007/978-3-319-59418-7.
  25. Moon, D.-W., Pyo, S.-H., Hong, D.-K., Bataa, O., & Norinpel, E. (2025). Assertion-based verification of I2C module using SystemVerilog. Electronics, 14(8), article number 1687. doi: 10.3390/electronics14081687.
  26. Mukherjee, R., Purandare, M., Polig, R., & Kroening, D. (2017). Formal techniques for effective co-verification of hardware/software co-designs. In Proceedings of the 54th annual design automation conference 2017 (article number 35). New York: Association for Computing Machinery. doi: 10.1145/3061639.3062253.
  27. Odarushchenko, O., Letychevskyi, O., Shamanskyi, V., Babeshko, I., Peschanenko, V., & Striuk, O. (2024). Information technology of formal verification and design of FPGA electronic projects. In 2024 14th international conference on dependable systems, services and technologies (pp. 1-6). New York: IEEE. doi: 10.1109/DESSERT65323.2024.11122210.
  28. Orenes-Vera, M., Manocha, A., Wentzlaff, D., & Martonosi, M. (2021). AutoSVA: Democratizing formal verification of RTL module interactions. In 2021 58th ACM/IEEE design automation conference (pp. 535-540). New York: IEEE. doi: 10.1109/DAC18074.2021.9586118.
  29. Radu, V., Dranga, D., Dumitrescu, C., Tabirca, A.I., & Stefan, M.C. (2024). Generative AI assertions in UVM-based System Verilog functional verification. Systems, 12(10), article number 390. doi: 10.3390/systems12100390.
  30. ter Beek, M.H., et al. (2025). Formal methods in industry. Formal Aspects of Computing, 37(1), article number 7. doi: 10.1145/3689374.
  31. Witharana, H., Lyu, Y., Charles, S., & Mishra, P. (2022). A survey on assertion-based hardware verification. ACM Computing Surveys, 54(11), article number 225. doi: 10.1145/3510578.
  32. Wu, N., Li, Y., Yang, H., Chen, H., Dai, S., Hao, C., Yu, C., & Xie, Y. (2024). Survey of machine learning for software-assisted hardware design verification: Past, present, and prospect. ACM Transactions on Design Automation of Electronic Systems, 29(4), article number 59. doi: 10.1145/3661308
  33. Yu, Z., Biere, A., & Heljanko, K. (2019). Certifying hardware model checking results. In Y. Ait-Ameur & S. Qin (Eds.), 21st international conference on formal engineering methods: Formal methods and software engineering (pp. 498-502). Cham: Springer. doi: 10.1007/978-3-030-32409-4_32.