Assertion-Driven Formal Verification for Custom RISC-V Core

In modern processor design, ensuring the correct functionality of each pipeline stage is crucial. Although simulation-based techniques are commonly employed to identify design flaws, they often fail to detect rare corner cases or subtle bugs that emerge only under specific conditions. This limitation poses a significant risk in safety-critical domains such as autonomous vehicles and medical devices, where failures can have severe consequences. To address these challenges, formal verification offers a mathematically rigorous and exhaustive method to validate hardware designs. This paper details a formal verification approach for a custom 5-stage pipelined RISC-V (RV32I) processor. The methodology leverages SystemVerilog Assertions (SVA) in conjunction with Cadence JasperGold to verify key components of the design, including instruction execution, pipeline control mechanisms, and data hazard management, ensuring reliable operation across all possible execution scenarios.