中央處理器 (Central Processing Unit, CPU) 為電腦的核心晶片，其基本功能在於處理電腦機器語言 (Machine language)，完成每一條指令的工作。然而隨著對中央處理器表現 (performance) 的要求日益增高，更多的優化 (optimization) 被加進中央處理器中，使其越來越複雜，在優化的過程中，執行指令的功能仍然要完全正確，即行為要完全符合指令規範，如何確保此事為本論文之主要目的。
在傳統方法中，當一顆中央處理器被設計完成，會經由模擬測資 (testbench
simulation) 來檢查中央處理器的指令執行功能，但此方法不但需要大量的測資，也無法涵蓋所有可能的情況 (corner case)。如今隨著正規驗證的工具日益成熟，我們可利用正規驗證理論來檢驗中央處理器，本論文所使用的方法 ISA-formal 即為利用正規驗證工具 JasperGold 檢查中央處理器的行為是否符合 ISA (Instruction Set Architecture) 的規範，同時降低亂序執行帶來的驗證複雜度。

ISA-formal is a formal verification method used to check the ISA of CPU. In order
to alleviate the state explosion problem of dealing with out-of-order feature of CPUs, we apply abstraction and reduction methods on verifying an open 32-bit RISC-V out-of-order superscalar processor named RSD. The processor has two in-order front-end pipelines used to decode and dispatch instructions, 16-entry OoO issue queues used to store instruction information and determine the order of issuing instruction, and five in-order back-end pipelines used to execute instructions and write the result data to register file. This paper presents five abstraction and reduction methods with sound and completeness proofs by compositional verification for the end-to-end ISA-formal to verify a superscalar out-of-order processor, using model checker tool to verify the properties against to the specification of RV32IM. The result shows that we can get a verified instruction in 775.6 seconds, it saves up to 99.1% of verification time and achieve full proof of ISA checking

[1] Sergey Berezin, Edmund Clarke, Armin Biere, and Yunshan Zhu. Verification of out-oforder processor designs using model checking and a light-weight completion function. Formal Methods in System Design, 20(2):159–186, 2002.
[2] Cadence. Jaspergold formal verification platform (apps). https://www.cadence.com/, 2016.
[3] 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.
[4] Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. ACM Sigplan Notices, 40(1):110–121, 2005.
[5] Yanyan Gao and Xi Li. Formal verification of out-of-order processor. In 2009 International Conference on Computer Modeling and Simulation, pages 129–135. IEEE, 2009.
[6] 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.
[7] Susumu Mashimo, Akifumi Fujita, Reoma Matsuo, Seiya Akaki, Akifumi Fukuda, Toru Koizumi, Junichiro Kadomoto, Hidetsugu Irie, Masahiro Goshima, Koji Inoue, et al. An open source fpga-optimized out-of-order risc-v soft processor. In 2019 International Conference on Field-Programmable Technology (ICFPT), pages 63–71. IEEE, 2019.
[8] Eric A Posner, Kathryn E Spier, and Adrian Vermeule. Divide and conquer. U of
Chicago Law & Economics, Olin Working Paper, (467):09–24, 2009.
[9] 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.
[10] Robert M Tomasulo. An efficient algorithm for exploiting multiple arithmetic units. IBM Journal of research and Development, 11(1):25–33, 1967.
[11] Andrew Waterman and Krste Asanovic. The risc-v instruction set manual. Volume I: User-Level ISA, Document Version 20191214-draft, 2019.