本論文探討了硬體設計中的驗證挑戰，及針對這些挑戰如何規劃有效的驗證流程。以嵌入式系統而言，為了達到低功耗會透過加入如壓縮指令集等方式，以便節省記憶體空間、縮短指令取得時間、降低處理器功耗。不過由於壓縮指令位元數的不同，進一步導致硬體架構設計更為複雜，因此對於指令對齊、解壓縮的正確性，以及我們如何改善原先端對端驗證方式應用於此架構，亦是本論文驗證的一大重點。
而在現代 AI 應用中，對於向量處理器（Vector Processor unit, VPU）的需求日益增加，本論文首次將端對端正規驗證方式應用於 VPU，確保向量指令 (SIMDinstruction) 的功能性符合 ISA SPEC 的要求。值得一提的是，我們所驗證的設計是RISC-V Vector extension 1.0-Frozen 版本的第一顆開源 VPU，而 RISC-V 向量擴展指令集又為當前 RISC-V 擴展環境中最長的指令集，因此對於 SPEC 標準的熟習程度和驗證難度均相當高。
然而，當正規驗證應用於大型系統時，存在著驗證複雜度過高，狀態空間爆炸等挑戰，因此本論文採用了多種抽象化技術以極力降低驗證複雜度的同時確保驗證準確性。僅比較其中我們提出較直覺對暫存器抽象的方式進行比較，針對 R-type 指令在相同 cycle 下可以達到 93% 的驗證時間縮減。
透過本論文應用的正規端對端驗證流程，在開源的處理器及向量加速處理器，分別為 CVA6 (CPU) 與 Ara (VPU)，皆找到其 RTL 硬體實作之錯誤。在 CVA6 上找到有號除法計算的運算錯誤；在 Ara 上我們透過斷言所涵蓋之 COI (Cone of influence)範圍便找到大量錯誤，並且我們找到的這些錯誤也被開發團隊承認的確需要修復，除此之外我們還提出了針對這些錯誤可行的改善方式，以及分析這些解決方式在硬體電路實現上所可能帶來的結果

In this thesis, we have made several significant contributions. Firstly, we developed a Verification Intellectual Property (VIP) tailored for RV64IMC, allowing users to customize configurations based on their specific requirements, providing high flexibility and adaptability. Secondly, we pioneered the application of end-to-end formal verification on the RISC-V Vector Processor Unit (VPU), marking a major breakthrough and uncovering various critical issues within the design. Through this verification approach, we successfully identified these issues and proposed corresponding solutions, enhancing the robustness of the design. Lastly, we introduced an intuitively designed abstracted register, significantly reducing the complexity of end-to-end verification. Throughout the thesis, we employed multiple abstraction techniques, including bit-width abstraction, Initial Value Abstractions (IVA), and property splitting. These abstraction methods enabled this study to delve deep into bound exploration, even under extremely high verification complexity, uncovering potential issues. These contributions not only enrich the research landscape in the RISC-V domain but also pave the way for novel applications of formal verification methods in hardware design.

[1] ARM Architecture Reference Manual Thumb-2 Supplement. [Online]. Available https://developer.arm.com/documentation/ddi0308/d/Introduction-to-Thumb-2/AboutThumb-2.
[2] Endianness. [Online]. Available https://en.wikipedia.org/wiki/Endianness.
[3] MMX Technology Technical Overview. [Online]. Available https://www.intel.com/content/dam/develop/external/us/en/documents/mmx-manualtech-overview-140701.pdf.
[4] The ARM and Thumb instruction sets. [Online]. Available https://developer.arm.com/documentation/ddi0406/b/Application-LevelArchitecture/Introduction-to-the-ARM-Architecture/The-ARM-and-Thumbinstruction-sets.
[5] The MIPS16e™ Application-Specific Extension to the MIPS32®Architecture , July 16,2013. [Online]. Available https://mips.com/products/architectures/ase/ase16e/.
[6] Cadence. Jaspergold formal verification platform (apps). https://www.cadence.com/,2016.
[7] K. Asanovic et al. RISC-V Vector Extension 1.0, Sep 20, 2021. [Online]. Available https://github.com/riscv/riscv-v-spec/releases/tag/v1.0.
[8] Yean-Ru Chen et al. Automate and accelerate risc-v verification by compositional formal methods. https://dvcon-proceedings.org/document/automate-and-accelerate-riscv-verification-by-compositional-formal-methods-presentation/, 2019. DVCON, Europe.
[9] Mihaela Gheorghiu Bobaru, Corina S Păsăreanu, and Dimitra Giannakopoulou. Automated assume-guarantee reasoning by abstraction refinement. In International Conference on Computer Aided Verification, pages 135–148. Springer, 2008.
[10] Matteo Perotti, Matheus Cavalcante, Nils Wistoff, Renzo Andri, Lukas Cavigelli, and Luca Benini. A “new ara＂for vector computing: An open source highly efficient risc-v v 1.0 vector processor design. In 2022 IEEE 33rd International Conference on Application-specific Systems, Architectures and Processors (ASAP), pages 43–51, 2022.
[11] Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. End-to-end verification of processors with isa-formal. In International Conference on Computer Aided Verification, pages 42–58. Springer, 2016.
[12] RISC-V. Available: https://riscv.org/.
[13] Richard M Russell. The cray-1 computer system. Communications of the ACM,21(1):63–72, 1978.
[14] Andrew Waterman. Ratified versions of the RV32I and RV64I base ISAs and MAFDQC standard extensions, Dec 14, 2019. [Online]. Available https://github.com/riscv/riscvisa-manual/releases/tag/Ratified-IMAFDQC.
[15] Florian Zaruba and Luca Benini. The cost of application-class processing: Energy and performance analysis of a linux-ready 1.7-ghz 64-bit risc-v core in 22-nm fdsoi technology. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 27(11):2629–2640, 2019.