Received 17.02.2026, Revised 26.05.2026, Accepted 25.06.2026 Published 03.08.2026

Methods of functional and formal verification of digital systems: Theoretical analysis and experimental application to modules of varying complexity

Oleksandr Ostrianko*

oleksandrostrianko@outlook.com



The study aimed to provide a theoretical justification of the nature of functional and formal verification of digital systems, to compare their methods, and to determine the possibilities for their coordinated application to digital modules of varying structural complexity. Methodology was based on normative-terminological, structural-analytical, functionalverification, formal logical and comparative-analytical methods, which made it possible to distinguish between scenariobased and property-based approaches to verifying hardware logic and to conduct an experimental and demonstrative verification of three test digital modules. The study established that functional verification ensured the verification of a digital module's behavioural compliance with the specification through test inputs, expected output responses, test benches, simulation and analysis of functional mode coverage. Formal verification yielded a different type of verification conclusion, as it was aimed at confirming or refuting correctness properties, invariants, logical and temporal conditions, valid transitions and the unreachability of erroneous states. Experimental and demonstrative verification on a multiplexer, a finite-state machine and a simplified interface controller showed that, as the complexity of the digital module increased, the number of functional scenarios grew, mode coverage became more challenging, and the risk of failing to detect hidden states, deadlocks or rare signal combinations increased. For the multiplexer, both approaches yielded consistent results; for the finite-state machine, the verification of resets, states and transitions was enhanced; for the interface controller, formal verification improved the assessment of deadlocks, signal conflicts and erroneous modes. The feasibility of a combined strategy, in which functional scenarios, coverage analysis, formal properties and the interpretation of possible counterexamples complement one another, has been demonstrated. The practical significance of the results is determined by their application in digital design, hardware verification and educational and research environments for planning the verification of digital modules, refining specifications, conducting coverage analysis, interpreting counterexamples and making decisions regarding the correctness of hardware logic

hardware logic; test scenarios; coverage analysis; correctness properties; counterexamples; control signal
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.

References

  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.