現有的處理器驗證方法在狀態空間爆炸（state-space explosion）和測試覆蓋率方面面臨嚴峻挑戰，尤其是在當前高度複雜的微架構設計中，這些挑戰進一步加劇了驗證的難度。形式驗證（Formal Verification） 雖然能夠提供精確的數學級正確性保證，但由於狀態空間的指數級增長，使得其在大規模設計上的應用受到極大限制。此外，形式驗證的計算開銷高，難以適用於完整的處理器核心，因此通常僅用於驗證關鍵模組或安全性敏感的區域。而傳統的基於模擬的方法，如模糊測試（Fuzz Testing），則透過隨機化測試來擴展驗證範圍，能夠在短時間內生成大量測試向量。然而，這種方法缺乏有效的測試引導機制，使得它難以針對複雜的控制流進行測試，特別是在涉及少見狀態轉換的場景時，可能會錯過潛在的錯誤，從而留下測試盲點。

為了解決這些問題，我們提出了一種基於形式引導的測試序列優化（Formal-Guided Test Sequence Optimization，FGTSO） 框架，該框架透過整合形式驗證與基於模擬的測試生成，實現對測試覆蓋盲點的系統性探索與補充，並提升整體驗證效率。FGTSO 的核心概念在於透過即時覆蓋率回饋機制，動態調整測試過程中的假設生成（Assumption Generation）、抽象建模（Abstraction Modeling）和 UVM 約束適配（UVM Constraint Adaptation），確保測試過程能夠持續聚焦於未覆蓋的區域，從而達到更精確的測試探索效果。相較於傳統獨立運行的形式驗證與模擬測試方法，FGTSO 創造了一個動態的雙向驗證反饋機制，使得這兩種技術能夠相輔相成，有效減少測試冗餘，並確保對難以觸發的角落案例（Corner Case）進行深入驗證。

我們在 CVA6 RISC-V 核心上對 FGTSO 進行了實驗測試，結果顯示該框架能夠在8 天內達到 99.91% 的分支覆蓋率（Branch Coverage），相較於 HyPFuzz 提升了 4.7%，顯示出 FGTSO 在驗證效率與測試精準度上的優勢。此外，FGTSO 在所有測試場景下均能達到高程式碼覆蓋率，包括行覆蓋率（Line Coverage）、切換覆蓋率（Toggle Coverage）、條件覆蓋率（Condition Coverage）和分支覆蓋率（Branch Coverage），確保了測試過程對處理器設計的全面驗證。這些結果證明，FGTSO 不僅能夠有效提高測試覆蓋率，還能夠識別傳統覆蓋率驅動或隨機測試方法難以捕捉的複雜角落案例行為，大幅提升整體驗證的可信度與可靠性。

Existing processor verification techniques face significant challenges due to state-space explosion and test coverage limitations, especially in modern complex microarchitectures. While formal verification provides strong correctness guarantees, its scalability is hindered by exponential state-space growth and substantial computational overhead, making it impractical for verifying entire processor cores. On the other hand, fuzz testing generates diverse test cases through randomization but lacks a structured approach to efficiently cover rare state transitions and intricate control flows, resulting in coverage gaps.
To overcome these limitations, we introduce Formal-Guided Test Sequence Optimization (FGTSO), a framework that combines formal verification with simulation-driven test generation to dynamically refine test sequences based on real-time coverage insights. By optimizing assumption generation, abstraction modeling, and UVM constraint adaptation, FGTSO systematically identifies and addresses uncovered regions, minimizing test redundancy while maximizing corner-case detection.
Experiments conducted on the CVA6 RISC-V core demonstrate that FGTSO attains 99.91% branch coverage in just 8 days, surpassing HyPFuzz by 4.7%. It also achieves comprehensive structural coverage, including line, toggle, condition, and branch coverage, ensuring thorough validation. These results establish FGTSO as an effective solution for improving test coverage, detecting complex corner cases, and enhancing verification efficiency, outperforming conventional verification methods.

[1] Hu-Hsi Yeh and Chung-Yang Huang. Automatic constraint generation for guided random simulation. In 2010 15th Asia and South Pacific Design Automation Conference(ASP-DAC), pages 613–618. IEEE, 2010.
[2] Rahul Kande, Addison Crump, Garrett Persyn, Patrick Jauernig, Ahmad-Reza Sadeghi,Aakash Tyagi, and Jeyavijayan Rajendran. {TheHuzz}: Instruction fuzzing of processors using {Golden-Reference} models for finding {Software-Exploitable} vulnerabilities. In 31st USENIX Security Symposium (USENIX Security 22), pages 3219–3236,2022.
[3] Chen Chen, Rahul Kande, Nathan Nguyen, Flemming Andersen, Aakash Tyagi,Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran. {HyPFuzz}:{Formal-Assisted}processor fuzzing. In 32nd USENIX Security Symposium (USENIX Security 23), pages 1361–1378, 2023.
[4] Florian Zaruba and Luca Benini. The cost of application-class processing: Energy and erformance 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):26292640, 2019.
[5] UC Berkeley Architecture Research Group. Risc-v torture: Random instruction set testing tool for risc-v. https://github.com/ucb-bar/riscv-torture, 2017. Accessed: 2025-01-23.
[6] Google. Risc-v dv: A random instruction generator for risc-v verification. https://github.com/google/riscv-dv, 2019. Accessed: 2025-01-23.
[7] RISC-VInternational. RISC-V Official Website, 2024. [Online; accessed 6-Feb-2025].
[8] Jaewon Hur, SuhwanSong, DongupKwon, EunjinBaek, Jangwoo Kim, and Byoungyoung Lee. Difuzzrtl: Differentialfuzztestingtofindcpubugs. In2021IEEESymposium on Security and Privacy (SP), pages 1286–1303. IEEE, 2021.
[9] OpenRISCProject. OpenRISC Official Website, 2024. [Online; accessed 6-Feb-2025].
[10] ARMLtd. AMBA AXI and ACEProtocol Specification, 2022.
[11] RISC-V Foundation. The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, 1.12 edition, 2021.
[12] Cadence Design Systems. Jaspergold verification platform. https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-verification-platform.html, 2024. Accessed: 2024-02-04.
[13] Synopsys. Vcs functional verification solution. https://www.synopsys.com/verification/simulation/vcs.html, 2024. Accessed: 2024-02-04.