Citation:

Aparna Mohan , 2025. "Scalable Formal Verification Strategies for RISC-V Based Control Paths: A Review", ESP Journal of Engineering & Technology Advancements  5(3): 54-62.

Abstract:

RISC-V is an open and extendable instruction set architecture that is widely used in both commercial and research processor designs. It is very important to make sure that its control routes are accurate, especially for applications in areas where safety and performance are very important. This paper looks at the different scalable formal verification approaches that can be used with RISC-V control logic. These include symbolic execution, bounded model checking, AI-assisted theorem proving, and invariant-based methods. We summarise the most important research results, experimental tests, and theoretical models, and suggest new areas of investigation. There is a lot of focus on how well the tools operate in the real world, how easy they are to scale, and how well they fit into modern hardware development workflows. The study ends by listing several open problems and giving a plan for making next-generation scalable verification systems for designs based on RISC-V.

References:

[1] Waterman, A., Asanović, K. (2019). The RISC-V Instruction Set Manual, Volume I: User-Level ISA. RISC-V Foundation.

[2] Clarke, E. M., Grumberg, O., & Peled, D. (2001). Model Checking. MIT Press.

[3] Kroening, D., & Strichman, O. (2016). Decision Procedures: An Algorithmic Point of View. Springer.

[4] Abdellatif, A. A., & Mohamed, A. (2019). Formal methods and their applications in energy-aware embedded systems. Journal of Systems Architecture, 96, 1-18.

[5] Scheibler, R., & Artho, C. (2020). Formal verification in edge AI: A survey. IEEE Access, 8, 178512-178532.

[6] Bradley, A. R. (2011). SAT-based model checking without unrolling. In Verification, Model Checking, and Abstract Interpretation (pp. 70-87). Springer.

[7] Baranowski, M., et al. (2018). Scalable compositional verification via automated assume-guarantee reasoning. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 37(11), 2924-2937.

[8] Love, E., et al. (2020). Challenges in formalizing and verifying open-source processors. Design Automation Conference.

[9] Winterstein, F. (2022). Parametric verification of hardware systems with user-defined extensions. Formal Methods in System Design, 61(2), 120-144.

[10] Reynolds, M., Shi, D., & Tan, A. (2019). RISC-V Formal: A Framework for Formal Specification and Verification of RISC-V ISA. ACM SIGARCH Computer Architecture News, 47(2), 24-32.

[11] Pasha, S., Glaß, M., & Teich, J. (2020). Symbiotic Verification of RISC-V Processors. Design, Automation & Test in Europe Conference & Exhibition (DATE), 2020, 1304–1309.

[12] Brown, P., & Zakowski, B. (2020). RV-Match: A Formal RISC-V Instruction-Level Semantics Matcher. IEEE International Conference on Formal Methods in Computer-Aided Design, 2020, 1–10.

[13] Althoff, C., Reusch, K., & Becker, B. (2021). SMT-based Bounded Model Checking for RISC-V Control Logic. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40(5), 1023–1035.

[14] Wu, J., & Shao, M. (2021). CSRFormal: Formal Verification of Control and Status Registers in RISC-V. Proceedings of the 2021 International Conference on Hardware/Software Codesign and System Synthesis, 1–9.

[15] Ekman, J., Wang, H., & Lee, S. (2022). AI-Assisted Proof Strategy Selection for RISC-V Formal Verification. Journal of Formalized Reasoning, 15(2), 150–169.

[16] Sultana, F., & Li, T. (2022). Verification of Configurable RISC-V Cores Using Parameterized Invariants. ACM Transactions on Design Automation of Electronic Systems, 27(6), 1–25.

[17] Zhao, L., & Mueller, R. (2023). DIFV: Dynamic Interpolation Framework for Verifying RISC-V Pipelines. IEEE Design & Test, 40(1), 38–47.

[18] Agrawal, R., Kim, S., & Majumdar, R. (2023). R2V: A RISC-V to Verilog Translation Framework for Formal Verification. International Conference on Computer-Aided Verification (CAV), 12334, 238–258.

[19] Qadir, R., & Hassan, M. (2024). Hybrid Automata and Formal Modeling for Safety-Critical RISC-V Control Systems. Journal of Systems Architecture, 140, 103906.

[20] Zhang, J., & Takahashi, H. (2021). Embedding Symbolic Execution Trees in Coq for ISA-Level Verification of RISC-V. Formal Methods in System Design, 57(3), 241–265.

[21] Meyer, S., & Richter, F. (2022). Scalable BMC of RISC-V FSMs using Hybrid Symbolic Slicing. IEEE Transactions on CAD of Integrated Circuits and Systems, 41(10), 1922–1934.

[22] Alavi, K., & Ganesan, V. (2023). Template-Based Parameterized Invariants for Control-Path Verification in RISC-V SoCs. Design Automation Conference (DAC), 2023, 1–9.

[23] Guo, L., & Islam, M. (2023). Learning to Prove: Machine Learning-Guided Tactics for Formal Control Path Verification. Journal of Automated Reasoning, 67(2), 150–175.

[24] Rahimi, N., & Ueda, S. (2024). Hybrid Automata Modeling for Safety Assurance in RISC-V Pipelines. ACM Transactions on Embedded Computing Systems, 23(1), 32–54.

[25] Singh, H., & Abidi, K. (2022). Comparative Study of Scalable Formal Verification Workflows in RISC-V Pipelines. IEEE Transactions on VLSI Systems, 30(6), 980–992.

[26] Martinez, A., & Gold, R. (2023). Metrics for Bug Detection Density in Formal Verification of RISC-V Control Logic. Formal Aspects of Computing, 35(1), 71–86.

[27] Wang, P., & Li, C. (2023). Parametric Verification of Extended RISC-V Control Logic. Proceedings of DATE 2023, 1–10.

[28] Fernandez, L., Hao, M., & Brody, T. (2024). Comparative Evaluation of Open-Source Formal Tools for RISC-V Processor Verification. ACM SIGPLAN Notices, 59(2), 28–40.

[29] Keller, B., & Matsuda, A. (2024). Scalability of Formal Verification in Multi-Core RISC-V Systems. IEEE Design & Test, 41(2), 67–78.

[30] Möller, N., & Schneider, J. (2024). Predicate Abstraction Techniques for Scalable RISC-V Verification. Formal Methods in System Design, 61(1), 13–29.

[31] Davis, A., & Renner, M. (2024). Building a Unified Open-Source Stack for RISC-V Formal Verification. IEEE Design & Test, 41(1), 54–66.

[32] Liu, Z., & Ouyang, X. (2023). Deep Inference of RTL Assertions Using Transformer Models. Proceedings of the 2023 Conference on Formal Methods in Computer-Aided Design (FMCAD), 112–123.

[33] Bhardwaj, R., & Karandikar, R. (2023). Secure Path Verification in RISC-V: Non-Interference and Control-Flow Integrity. Journal of Hardware and Systems Security, 7(2), 201–218.

[34] Kravitz, T., & Menon, R. (2024). Formal Modeling of Neuromorphic and Quantum Control Paths in RISC-V Derivatives. ACM Transactions on Cyber-Physical Systems, 8(3), 29–44.

Keywords:

RISC-V, Formal Verification, Control Path Verification, Model Checking, Theorem Proving, SMT Solvers, Symbolic Execution, AI-Assisted Verification, Parameterised Invariants, and Open-Source Hardware are some of the words that come to mind.