本論文以ARM的ISA-Formal和Clifford Wolf所提出用於驗證RISC-V指令集架構正確性的正規驗證介面 (RISC-V Formal Interface, RVFI) 之概念為基礎，提出一個不同於他們且針對採用RISC-V架構處理器進行功能驗證的自動化正規驗證流程。相較於ARM與Clifford Wolf 的方法，我們除了完整驗證RV32I指令集，並延伸驗證範圍，將他們沒有驗證的項目進行驗證，包括 control status register (CSR，控制狀態暫存器) 、系統呼叫與exceptions (例外) 等相關指令。同時，我們針對驗證需求，擴展定義額外所需的RVFI驗證介面，並且相較於以上兩篇work在狀態空間爆炸問題皆無明確描述解決方法，我們為了減緩驗證狀態空間爆炸的問題，在自動產生驗證特性/斷言的流程中嵌入斷言抽象化的技術，有效地減少驗證空間。在單驗證add指令情況之下，可以達到減少 98.4% 驗證時間。然而，即使在這個案例中能減少如此可觀的驗證時間，仍然有少數的斷言無法達到 full proof (完全驗證)。針對這些因為狀態空間爆炸問題導致驗證無法在時限內收斂的情況，我們佐以分析涵蓋率的資訊來支持bounded verification (有限驗證) 結果的信心。
同時，透過本篇論文提出的自動化正規驗證流程，我們在兩個開源的處理器，Vscale及RV12，皆有找到其實作的錯誤。在Vscale中我們發現它對於sra、srai和jalr指令的相關設計有誤；在RV12 中我們發現它對於csrrwi指令的設計有錯誤。

RISC-V is an open-source instruction set architecture (ISA) initialized by UC-Berkeley. We borrow the concept of ARM’s ISA-Formal and extend a RISC-V interface called RVFI to verify the correctness of RISC-V’s implementations. Our proposed work can not only automatically generate the RISC-V RV32I properties for model checking but also accelerate the verification tasks to be convergent efficiently with compositional formal methods. The experimental results show that RISC-V formal properties are completely auto-generated and correctly verified by Cadence JasperGold. We not only detect the sra, srai and jalr defects in the latest version of Vscale in 7.1 hours but also find an error in csrrwi in the latest version of RV12.

[1] H. D. Foster, "Trends in functional verification: A 2014 industry study," in Proceedings of the 52nd Annual Design Automation Conference: ACM, p. 48, 2015.
[2] Cadence. JasperGold Formal Verification Platform (Apps) [Online]. Available: https://www.cadence.com/content/cadence-www/global/zh_TW/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html.
[3] H. D. Foster. (2016). Part 9: The 2016 Wilson Research Group Functional Verification Study [Online]. Available: https://blogs.mentor.com/verificationhorizons/blog/2016/10/10/part-9-the-2016-wilson-research-group-functional-verification-study/.
[4] A. Reid et al., "End-to-end verification of processors with ISA-formal," in International Conference on Computer Aided Verification: Springer, pp. 42-58, 2016.
[5] RISC-V. RISC-V [Online]. Available: https://riscv.org/.
[6] C. Wolf. (2016). RISC-V Formal Verification Framework [Online]. Available: https://github.com/SymbioticEDA/riscv-formal.
[7] UCB-BAR. (2015). Verilog version of Z-scale [Online]. Available: https://github.com/ucb-bar/vscale.
[8] RoaLogic. (2017). RV12 RISC-V Processor [Online]. Available: https://roalogic.com/portfolio/riscv-processor/.
[9] ARM. Arm: Architecting a Smarter World [Online]. Available: https://www.arm.com/.
[10] UCB-BAR. Berkeley Architecture Research [Online]. Available: https://bar.eecs.berkeley.edu/.
[11] A. Waterman and K. Asanovic, "The RISC-V Instruction Set Manual-Volume I: User-Level ISA-Document Version 2.2," RISC-V Foundation (May 2017), 2017.
[12] C. Wolf. (2017). SymbiYosys [Online]. Available: https://symbiyosys.readthedocs.io/en/latest/index.html.
[13] M. Chupilko, A. Kamkin, A. Kotsynyak, and A. Tatarnikov, "MicroTESK: Specification-Based Tool for Constructing Test Program Generators," in Haifa Verification Conference: Springer, pp. 217-220, 2017.
[14] M. Chupilko, A. Kamkin, A. Kotsynyak, A. Protsenko, S. Smolov, and A. Tatarnikov, "Maintaining ISA Specifications in MicroTESK Test Program Generator," in 18th International Workshop on Microprocessor and SOC Test and Verification (MTV): IEEE, pp. 10-14, 2017.
[15] M. Freericks, "The nML machine description formalism," ed: Leiter der Fachbibliothek Informatik, Sekretariat FR 5-4, 1991.
[16] Y. A. Manerkar, D. Lustig, M. Martonosi, and M. Pellauer, "RTLCheck: Verifying the memory consistency of RTL designs," in Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture: ACM, pp. 463-476, 2017.
[17] U. Kühne, S. Beyer, J. Bormann, and J. Barstow, "Automated formal verification of processors based on architectural models," in Formal Methods in Computer Aided Design: IEEE, pp. 129-136, 2010.
[18] R. Baranowski and M. Trunzer, "Complete Formal Verification of a Family of Automotive DSPs," in DVCon Europe, 2016.
[19] S. Thompson, Haskell: the craft of functional programming. Addison-Wesley, 2011.
[20] P. L. a. V. G. a. M. CSAIL. (2017). A formal semantics of the RISC-V ISA in Haskell [Online]. Available: https://github.com/mit-plv/riscv-semantics.
[21] P. Mishra and N. Dutt, Processor description languages. Elsevier, 2011.
[22] S. I. s. C. S. Laboratory. (2015). An executable specification of the RISCV ISA in L3 [Online]. Available: https://github.com/SRI-CSL/l3riscv.
[23] A. Armstrong et al., "ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS," Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, p. 71, 2019.
[24] R. S. Nikhil. (2017). ISA Formal Spec Technical Group Update [Online]. Available: https://content.riscv.org/wp-content/uploads/2017/12/Wed-1442-RISCVRishiyurNikhil.pdf.
[25] E. Cerny, S. Dudani, J. Havlicek, and D. Korchemny, SVA: the power of assertions in systemVerilog. Springer, 2015.
[26] A. Waterman. (2017). The RISC-V Instruction Set Manual Volume II: Privileged Architecture Privileged Architecture Version 1.10 [Online]. Available: https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10.pdf.
[27] P. Bjesse, "A practical approach to word level model checking of industrial netlists," in International Conference on Computer Aided Verification: Springer, pp. 446-458, 2008.
[28] D. Giannakopoulou, C. S. Pasareanu, and J. M. Cobleigh, "Assume-guarantee verification of source code with design-level assumptions," in Proceedings. 26th International Conference on Software Engineering: IEEE, pp. 211-220, 2004.
[29] UCB-BAR. (2014). Z-scale Microarchitectural Implementation of RV32 ISA [Online]. Available: https://github.com/ucb-bar/zscale.