Formal Verification

Relevant source files

Ibex employs formal verification (FV) to ensure the architectural correctness and security of the core. The verification strategy is split into three primary areas: end-to-end trace equivalence against a formal specification (Sail), unit-level verification of the CSR (Control and Status Register) model, and Formal Property Verification (FPV) for the instruction cache.

1. End-to-End Trace Equivalence (Sail)

The primary formal effort for Ibex is an end-to-end proof of trace equivalence against the Sail RISC-V model This approach ensures that for any sequence of instructions, the memory operations and architectural state transitions produced by Ibex match those of the formal RISC-V specification dv/formal/README.md94-98

Implementation Architecture

The flow uses a tool called psgen to compile properties into SystemVerilog and the Sail compiler to generate a SystemVerilog reference model from the formal specification dv/formal/Makefile51-59

Data Flow and Hierarchy:

1. Reference Model: The Sail RISC-V model is translated to SystemVerilog (ibexspec.sv) dv/formal/Makefile51-53
2. Top-Level Wrapper: The top module in dv/formal/check/top.sv instantiates both the Ibex core (ibex_top) and the Sail specification dv/formal/check/top.sv8-14
3. Peek/Monitor Infrastructure: Internal signals from Ibex (pipeline stages, LSU, CSRs) are bound to the verification logic using macros dv/formal/check/top.sv21-36
4. Property Generation: Properties defined in .proof files (e.g., ibex.proof, riscv.proof) are processed by psgen into a TCL run script and SV assertions dv/formal/Makefile57-59

Code-to-Entity Mapping: End-to-End Proof

The following diagram illustrates how the formal testbench bridges the gap between the RTL implementation and the Sail formal specification.

Trace Equivalence Infrastructure

Sources: dv/formal/check/top.sv8-36 dv/formal/Makefile51-64

Key Proof Targets

• Wrap: Proves that on each specification invocation, the new inputs are consistent with previous outputs dv/formal/README.md105-106
• Live: Proves liveness—that the core will always eventually progress to a state where it can be compared against the spec dv/formal/README.md107-108
• Load/Store: Ensures memory requests made to the bus are correct given the current architectural state dv/formal/README.md108-110
• Top: A case-split proof asserting that every individual instruction retires correctly according to the ISA dv/formal/README.md115-117

Sources: dv/formal/README.md101-117 dv/formal/thm/riscv.proof138-175

2. CSR Register Model Verification

Ibex uses a dedicated formal-friendly testbench to verify the behavior of the Control and Status Registers (CSRs). This environment uses a C++ reference model linked via DPI to verify register access, side effects, and reset values.

Implementation

The testbench tb_cs_registers instantiates the ibex_cs_registers module and drives it using a DPI-based driver dv/cs_registers/tb/tb_cs_registers.sv65-86

Key Components:

CSR Verification Data Flow

Sources: dv/cs_registers/tb/tb_cs_registers.sv120-149 dv/cs_registers/tb_cs_registers.core15-31

3. Instruction Cache FPV

The instruction cache (ibex_icache) is verified using Formal Property Verification (FPV) assertions bound directly into the DUT. This targets the complex state machines governing prefetching, cache hits/misses, and ECC error handling.

Implementation Details

The formal testbench formal_tb is bound into the ibex_icache module formal/icache/formal_tb.sv5 It includes:

• Protocol Assumptions: Constraints on the instruction bus (e.g., instr_gnt_i vs instr_rvalid_i ordering) formal/icache/formal_tb.sv146-166
• State Machine Invariants: Assertions ensuring that the Fill Buffers (fill_busy_q) and prefetch logic (prefetch_addr_q) behave correctly under all valid bus responses formal/icache/formal_tb.sv55-70
• ECC Verification: If ICacheECC is enabled, formal properties verify that single-bit errors are corrected and double-bit errors trigger err_o formal/icache/formal_tb.sv23-42

Verification Environment Configuration

The FPV environment is configured via the ibex_icache_fpv.core file, which sets parameters like PMPEnable and ICacheECC to explore different architectural configurations during formal analysis formal/icache/ibex_icache_fpv.core

Sources: formal/icache/formal_tb.sv1-81 dv/formal/verify.tcl29-33

The Ibex formal flow supports both commercial (JasperGold) and open-source (Yosys + rIC3) tools.

The JasperGold flow uses a task-based approach, splitting the massive end-to-end proof into manageable "Steps" (Step 0 to Step 22) to aid convergence dv/formal/verify.tcl77-121

Sources: dv/formal/Makefile81-88 dv/formal/README.md19-38 Makefile82-84