Pipelined RISC-V CPU with Formal Verification

Overview

This project implements a 5-stage pipelined RISC-V CPU in SystemVerilog, supporting a subset of the RV32I ISA. The design includes robust hazard detection and resolution logic (stalling, flushing, and forwarding) and is prepared for formal verification using SystemVerilog Assertions (SVA) and SymbiYosys.

Architecture

The CPU follows a classic 5-stage pipeline:

graph LR
    IF[IF: Fetch] --> IFID((IF/ID Reg))
    IFID --> ID[ID: Decode]
    ID --> IDEX((ID/EX Reg))
    IDEX --> EX[EX: Execute]
    EX --> EXMEM((EX/MEM Reg))
    EXMEM --> MEM[MEM: Memory]
    MEM --> MEMWB((MEM/WB Reg))
    MEMWB --> WB[WB: Writeback]
    
    style IFID fill:#f9f,stroke:#333,stroke-width:2px
    style IDEX fill:#f9f,stroke:#333,stroke-width:2px
    style EXMEM fill:#f9f,stroke:#333,stroke-width:2px
    style MEMWB fill:#f9f,stroke:#333,stroke-width:2px

Loading

1. IF (Instruction Fetch): Fetches instructions from memory.
2. ID (Instruction Decode): Decodes instructions and reads from the register file.
3. EX (Execute): Performs ALU operations and calculates branch targets.
4. MEM (Memory Access): Reads/writes to data memory.
5. WB (Write Back): Writes results back to the register file.

Supported ISA (RV32I Subset)

• Arithmetic: ADD, SUB, AND, OR
• Immediate: ADDI
• Memory: LW, SW
• Control: BEQ, BNE

Hazard Handling

graph TD
    HU[Hazard Unit] -- Stall/Flush --> IF
    HU -- Stall/Flush --> IFID
    HU -- Flush --> IDEX
    
    FU[Forwarding Unit] -- Bypassing --> EX
    
    ID -- Operands --> HU
    EX -- Target/Result --> HU
    
    MEM -- Bypass Data --> FU
    WB -- Bypass Data --> FU
    EX -- Operand Addr --> FU

Loading

• RAW Hazards: Resolved using a dedicated forwarding_unit.sv that bypasses data from MEM and WB stages to EX.
• Load-Use Hazards: Detected by hazard_unit.sv, resulting in a 1-cycle stall and pipeline bubble.
• Control Hazards: Branch mispredictions/taken branches result in a pipeline flush of the IF/ID and ID/EX stages.

Project Structure

riscv-formal/
├── rtl/               # Core RTL modules
│   ├── cpu_top.sv     # Top-level integration
│   ├── alu.sv
│   ├── hazard_unit.sv
│   ├── forwarding_unit.sv
│   └── ...
├── assertions/        # SystemVerilog Assertions
│   ├── cpu_assertions.sv
│   └── cpu_bind.sv
├── formal/            # SymbiYosys configuration
│   └── cpu.sby
├── tb/                # Testbenches
│   └── cpu_pipelined_tb.sv
├── programs/          # Test programs (.mem)
└── waveforms/         # VCD output files

Verification

Directed Simulation

The design is verified using Icarus Verilog. A comprehensive test program in programs/test_programs.mem exercises all supported instructions and hazard scenarios.

Run Simulation:

iverilog -g2012 -o cpu_tb_out tb/cpu_pipelined_tb.sv rtl/*.sv
vvp cpu_tb_out

Formal Verification

Formal properties are defined in assertions/cpu_assertions.sv, covering:

• Safety: x0 immutability, PC alignment, branch target correctness.
• Liveness: Deadlock-free execution and forward progress.
• Control Flow: Valid PC progression.

Run Formal Proof (requires SymbiYosys):

cd formal
sby cpu.sby

Debugging

Waveforms are dumped to waveforms/cpu_waves.vcd and can be analyzed using GTKWave.

Waveform Analysis

The following waveform illustrates the pipeline execution of the test program, highlighting the hazard resolution logic:

Key Observations:

• T5 (Forwarding): Data is bypassed from the MEM stage to the EX stage for the ADD x3 instruction.
• T7 (Stall): A 1-cycle stall is inserted (pc_stall high) to resolve a Load-Use dependency for BEQ x4.
• T9 (Flush): The instruction in the decode stage is flushed (id_ex_flush high) after a branch is taken, ensuring the correct instruction flow.

Results

The pipelined CPU successfully executes complex instruction sequences with overlapping dependencies, maintaining architectural consistency and performance.