diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6229b35..659a019 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,10 +18,14 @@ jobs: lint: runs-on: ubuntu-24.04 container: { image: "verilator/verilator:v5.054", options: --entrypoint "" } + strategy: + fail-fast: false + matrix: + core: [cv32e40p, rabbit5] steps: - uses: actions/checkout@v4 with: { submodules: recursive } - - run: verilator --version && make lint + - run: verilator --version && make lint CORE=${{ matrix.core }} soc-sim: # One job per (core, program). Add cores here as rtl/cores// adapters land. @@ -30,7 +34,7 @@ jobs: strategy: fail-fast: false matrix: - core: [cv32e40p] + core: [cv32e40p, rabbit5] prog: [hello] steps: - name: RISC-V GCC @@ -45,7 +49,7 @@ jobs: name: soc-${{ matrix.core }}-${{ matrix.prog }} path: | dv/cocotb/soc/results.xml - sw/baremetal/build/${{ matrix.prog }}/${{ matrix.prog }}.dis + sw/baremetal/build/${{ matrix.core }}/${{ matrix.prog }}/${{ matrix.prog }}.dis ip-test: runs-on: ubuntu-24.04 @@ -64,6 +68,52 @@ jobs: - working-directory: hw_ip/sim run: uv run make TARGET=${{ matrix.target }} # non-zero exit on any failed test + # riscv-formal (45 checks) + rabbit5 timing properties. ~1 min on 4 cores. + formal: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + with: { submodules: recursive } + - uses: YosysHQ/setup-oss-cad-suite@v3 + with: { version: "2026-11-04" } # pinned: yosys, sby, boolector + - run: yosys -V && sby --version + - run: make formal + - uses: actions/upload-artifact@v4 + if: failure() + with: + name: formal-results + path: | + dv/formal/rabbit5/build/riscv-formal/cores/rabbit5/checks/*/logfile.txt + dv/formal/rabbit5/build/riscv-formal/cores/rabbit5/checks/*/engine_0/*.vcd + dv/formal/rabbit5/timing/timing_*/logfile.txt + dv/formal/rabbit5/timing/timing_*/engine_0/*.vcd + + # Gate-level smoke test: Yosys builds the netlist, the pinned Verilator image runs it. + gls-netlist: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - uses: YosysHQ/setup-oss-cad-suite@v3 + with: { version: "2026-11-04" } + - run: make gls-netlist CORE=rabbit5 + - uses: actions/upload-artifact@v4 + with: { name: gls-netlist-rabbit5, path: build/gls/rabbit5 } + + gls-smoke: + needs: gls-netlist + runs-on: ubuntu-24.04 + container: { image: "verilator/verilator:v5.054", options: --entrypoint "" } + steps: + - name: RISC-V GCC + run: apt-get update -q && apt-get install -y -q gcc-riscv64-unknown-elf libpython3.12-dev + - uses: actions/checkout@v4 + - uses: astral-sh/setup-uv@v6 + - uses: actions/download-artifact@v4 + with: { name: gls-netlist-rabbit5, path: build/gls/rabbit5 } + - run: uv sync + - working-directory: dv/cocotb/soc + run: uv run make CORE=rabbit5 PROG=hello GLS=1 + rma-smoke: runs-on: ubuntu-24.04 steps: diff --git a/.gitignore b/.gitignore index d0625c5..5f22c8c 100644 --- a/.gitignore +++ b/.gitignore @@ -35,3 +35,7 @@ assets/** sw/baremetal/build/ **/sim_build_*/ **/*.fst +build/ +dv/formal/rabbit5/build/ +dv/formal/rabbit5/timing/timing_*/ +dv/formal/rabbit5/timing/timing/ diff --git a/.gitmodules b/.gitmodules index 8f33b76..19b1c5c 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "third_party/cv32e40p"] path = third_party/cv32e40p url = https://github.com/openhwgroup/cv32e40p.git +[submodule "third_party/riscv-formal"] + path = third_party/riscv-formal + url = https://github.com/YosysHQ/riscv-formal.git diff --git a/Makefile b/Makefile index 165babb..880e7cf 100644 --- a/Makefile +++ b/Makefile @@ -5,6 +5,8 @@ # make ip-test run every hw_ip cocotb unit/integration test # make lint Verilator lint of the SoC # make rma-smoke run all rma_analysis example configs +# make formal riscv-formal + timing properties (CORE=rabbit5 only) +# make gls-smoke synthesize the core with Yosys, run firmware on the netlist # make ci everything CI runs REPO := $(abspath .) export REPO @@ -20,7 +22,7 @@ IP_TARGETS := pwm_unit qei_unit telemetry_rx telemetry_tx wb_telemetry rf_cdc \ RMA_XFAIL := fifo_same_priority_interference.yaml help: - @sed -n '2,9p' Makefile | sed 's/^# //' + @sed -n '2,11p' Makefile | sed 's/^# //' sync: uv sync @@ -58,11 +60,34 @@ rma-smoke: sync uv run rma_analysis $$f >/dev/null && echo "ok $$f"; \ done +# ---- formal (rabbit5) --------------------------------------------------------- +formal: + $(MAKE) -C dv/formal/rabbit5 + +# ---- gate-level smoke test: generic Yosys gates, zero delay ---------------------- +# Catches RTL that simulates differently from what synthesizes (latches, X, +# initial values, simulation-only constructs) long before a real PDK flow. +GLS_DIR := build/gls/$(CORE) +YOSYS_SLANG := $(shell yosys -p 'help read_slang' >/dev/null 2>&1 || echo -m slang) +gls-netlist: $(GLS_DIR)/rabbit_cpu_netlist.v +$(GLS_DIR)/rabbit_cpu_netlist.v: $(wildcard rtl/cores/$(CORE)/*.sv) + @mkdir -p $(GLS_DIR) + yosys $(YOSYS_SLANG) -q -l $(GLS_DIR)/synth.log -p "read_slang \ + $$(grep -v '^//' rtl/cores/$(CORE)/files.f | sed 's|$${REPO}|$(REPO)|' | tr '\n' ' ') \ + --top rabbit_cpu -DSYNTHESIS; \ + synth -top rabbit_cpu -flatten; tee -o $(GLS_DIR)/stat.txt stat; \ + write_verilog -noattr $@" + @grep -E '^ +[0-9]+ +cells' $(GLS_DIR)/stat.txt | head -1 + +gls-smoke: sync gls-netlist + cd dv/cocotb/soc && uv run $(MAKE) CORE=$(CORE) PROG=$(PROG) GLS=1 + ci: lint soc-sim ip-test rma-smoke clean: $(MAKE) -C sw/baremetal clean cd dv/cocotb/soc && rm -rf sim_build_* results.xml dump.fst + rm -rf build dv/formal/rabbit5/build dv/formal/rabbit5/timing/timing_* cd hw_ip/sim && uv run $(MAKE) clean -.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke ci clean +.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke formal gls-netlist gls-smoke ci clean diff --git a/README.md b/README.md index 497015b..4394185 100644 --- a/README.md +++ b/README.md @@ -2,20 +2,25 @@ An open, verifiable **real-time RISC-V SoC** for robotics: RTL → verification → FPGA → open-source ASIC, evaluated with Zephyr and real-time Linux, with a -vector / quantized-NN block. Five-year plan: -[`docs/research/2026-11-04-soc-5yr-plan.md`](docs/research/2026-11-04-soc-5yr-plan.md). +vector / quantized-NN block. Five-year plan and research notes are kept +outside the repository. -Baseline CPU: **OpenHW CV32E40P** (RV32IMC). Every layer above the CPU talks to -a core-agnostic `rabbit_cpu` contract, so other cores (Ibex, CV32E40X, our own -5-stage core) plug in the same way: [`rtl/cores/README.md`](rtl/cores/README.md). +CPUs: **rabbit5**, our own timing-predictable 5-stage RV32I core +([`rtl/cores/rabbit5/README.md`](rtl/cores/rabbit5/README.md)), and **OpenHW +CV32E40P** (RV32IMC) as reference. Every layer above the CPU talks to a +core-agnostic `rabbit_cpu` contract, so cores plug in the same way: +[`rtl/cores/README.md`](rtl/cores/README.md). ## Quick start ```bash git clone --recursive git@github.com:abmajith/rt-rabbit.git && cd rt-rabbit uv sync -make soc-sim # run sw/baremetal/hello on CV32E40P in Verilator -make ci # everything CI runs +make soc-sim # run sw/baremetal/hello on CV32E40P in Verilator +make soc-sim CORE=rabbit5 # ... on our own core +make formal # riscv-formal + timing properties for rabbit5 (~35 s) +make gls-smoke CORE=rabbit5 # same firmware on the synthesized gate netlist +make ci # lint + simulation tests ``` Walkthrough: [`docs/GETTING_STARTED.md`](docs/GETTING_STARTED.md) · diff --git a/asic/README.md b/asic/README.md index 8ee7ddc..9117b3a 100644 --- a/asic/README.md +++ b/asic/README.md @@ -4,4 +4,4 @@ learn LibreLane end to end. - Y4: full MCU SoC on an IHP or sky130 (ChipFoundry) shuttle. - Keep RTL PDK-portable (no vendor macros in core logic; SRAMs behind a wrapper). -Shuttle landscape as of 2026: see `docs/research/2026-11-04-soc-5yr-plan.md` §1.6. +Shuttle landscape as of 2026 (Efabless closed; Tiny Tapeout on IHP; sky130 via ChipFoundry): see the research notes kept outside the repo. diff --git a/docs/GETTING_STARTED.md b/docs/GETTING_STARTED.md index 3d23e41..0c06aca 100644 --- a/docs/GETTING_STARTED.md +++ b/docs/GETTING_STARTED.md @@ -26,7 +26,7 @@ make ci # lint + SoC firmware sim + 10 hw_ip tests + rma_analysis examp | 1 | `sw/baremetal/hello/main.c` | The C program: prints, self-checks, cycle count | | 2 | `sw/baremetal/common/crt0.S` | Reset → stack → zero .bss → `main` → write exit code | | 3 | `sw/baremetal/common/link.ld` | Vectors at 0x0, code at 0x80 (CPU boot address) | -| 4 | `sw/baremetal/build/hello/hello.dis` | The actual instructions (after `make firmware`) | +| 4 | `sw/baremetal/build/cv32e40p/hello/hello.dis` | The actual instructions (after `make firmware`) | | 5 | `rtl/soc/rabbit_soc_sim.sv` | CPU + RAM + sim-control, address decode | | 6 | `rtl/cores/cv32e40p/rabbit_cpu.sv` | How a vendor core is plugged into our contract | | 7 | `dv/cocotb/soc/test_soc.py` | Testbench: clock, reset, console capture, pass/fail | diff --git a/docs/STATUS.md b/docs/STATUS.md index de4af37..acb7df5 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -1,4 +1,4 @@ -# Status (updated 2026-11-04) +# Status (updated 2026-11-06) ## Works @@ -10,6 +10,19 @@ | rma_analysis examples | `make rma-smoke` | 11 run, 1 expected failure | | GitHub Actions | `.github/workflows/ci.yml` | lint, soc-sim matrix, ip-test matrix, rma-smoke | +## rabbit5 (own core) — M0 done on branch `rabbit5-m0` + +| Item | Command | Result | +|---|---|---| +| hello on rabbit5 (RV32I, 5-stage) | `make soc-sim CORE=rabbit5` | PASS, 3958 cycles | +| riscv-formal | `make formal` | 45/45 PASS | +| timing properties T1–T3 + covers | `make formal` | PASS (BMC 24) | +| gate-level smoke (Yosys generic netlist) | `make gls-smoke CORE=rabbit5` | PASS, same 3958 cycles | + +Next (M1/M2): enable riscv-formal CSR checks, timer + external interrupt with a +proven entry-latency bound, RISCOF compliance, then the dual-core TDM work (M4). +Review guide: `rtl/cores/rabbit5/README.md`. + ## Known issues - `hw_ip/sim` targets `telemetry_rf` and `top` need @@ -29,6 +42,7 @@ - [x] Bare-metal toolchain flow (GCC → hex → $readmemh) - [x] Firmware-driven cocotb SoC test - [x] CI pipeline +- [x] Own core rabbit5 v0 with riscv-formal, timing properties, GLS smoke (2026-11-06) - [ ] Machine timer (mtime/mtimecmp) + interrupt test (irq_i already exposed) - [ ] OBI→Wishbone bridge; attach PWM / QEI / telemetry to the CPU - [ ] UART (needed for FPGA and Zephyr console) diff --git a/dv/cocotb/soc/Makefile b/dv/cocotb/soc/Makefile index 5357a49..d3e7111 100644 --- a/dv/cocotb/soc/Makefile +++ b/dv/cocotb/soc/Makefile @@ -8,7 +8,7 @@ PROG ?= hello include $(REPO)/rtl/cores/$(CORE)/core.mk -FIRMWARE := $(REPO)/sw/baremetal/build/$(PROG)/$(PROG).hex +FIRMWARE := $(REPO)/sw/baremetal/build/$(CORE)/$(PROG)/$(PROG).hex export RABBIT_FIRMWARE := $(FIRMWARE) export RABBIT_PROG := $(PROG) @@ -19,9 +19,16 @@ COCOTB_TEST_MODULES = test_soc SIM_BUILD ?= sim_build_$(CORE) # Sources come from the per-core and SoC file lists (${REPO} is expanded by Verilator). +# GLS=1 replaces the core RTL by its gate-level netlist (see `make gls-netlist`). VERILOG_SOURCES = -EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f -f $(REPO)/rtl/soc/files.f -EXTRA_ARGS += $(CORE_VERILATOR_FLAGS) -DRABBIT_QUIET +ifeq ($(GLS),1) +NETLIST := $(REPO)/build/gls/$(CORE)/rabbit_cpu_netlist.v +EXTRA_ARGS += $(NETLIST) -Wno-fatal -DRABBIT_GLS +SIM_BUILD = sim_build_$(CORE)_gls +else +EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f $(CORE_VERILATOR_FLAGS) +endif +EXTRA_ARGS += -f $(REPO)/rtl/soc/files.f -DRABBIT_QUIET ifeq ($(WAVES),1) # Build with tracing, switch it on at run time, and keep a separate build dir # (a traced model is slower, so the normal build stays trace-free). diff --git a/dv/formal/README.md b/dv/formal/README.md index 6d6b301..706952c 100644 --- a/dv/formal/README.md +++ b/dv/formal/README.md @@ -1,8 +1,39 @@ -# dv/formal — formal verification (planned) - -- SymbiYosys properties for our own RTL first: OBI protocol (req held until - gnt, exactly one rvalid per granted request), address decode, sim-control. -- Coprocessor-port handshake properties when the VPU lands (Y2). -- **riscv-formal** for rabbit5 (Y1 H2), via its RVFI port. -- Long term: bounded proofs of worst-case interrupt latency (see - `docs/research/2026-11-04-soc-5yr-plan.md` §6). +# dv/formal — formal verification + +## rabbit5 (working) + +```bash +make formal # from the repo root: everything below (~35 s on 22 cores) +make -C dv/formal/rabbit5 riscv-formal +make -C dv/formal/rabbit5 timing +make -C dv/formal/rabbit5 check C=insn_add_ch0 # one check +``` + +| Part | What it proves | Files | +|---|---|---| +| **riscv-formal** (YosysHQ, submodule) | every RV32I instruction computes what the ISA says (37 checks), plus pipeline consistency: `reg` (forwarding), `pc_fwd`/`pc_bwd` (branches, flushes), `causal`, `unique`, `liveness`, `ill` | `rabbit5/checks.cfg`, `rabbit5/wrapper.sv` | +| **timing properties** (ours) | T1 exact retirement-gap model, T2 first retirement at cycle 5, T3 memory used exactly one cycle before retirement; covers prove every case and the 6..16 throughput bounds are reachable | `rabbit5/timing/` | + +How it fits together: +1. rabbit5 is written in modern SystemVerilog. riscv-formal reads cores with + Yosys' built-in parser, so the Makefile first converts the core with the + **slang** frontend into one plain Verilog file (`build/rabbit5_flat.v`). +2. `genchecks.py` expects `/cores//`; the Makefile builds a + small mirror in `build/` (symlinks to the submodule), so the submodule is + never modified. +3. The timing proof reads the SystemVerilog directly through slang (≈10 s; + the converted file made the solver ~60x slower). + +Bounded proofs: all results hold for every instruction stream up to the +configured depth (12–20 cycles for riscv-formal, 24 for timing), not for +unbounded time. + +Mutation results (to show the checks are not vacuous): +- forwarding priority MEM/WB swapped → only `reg_ch0` fails; +- stall on every EX dependency (not just loads) → timing T1 fails, riscv-formal passes. + +## Planned + +- CSR checks (`csrw`, `csrc_*`) when interrupts land (M2). +- SymbiYosys properties for the OBI bus and the SoC address decode. +- Dual core (M4): TDM arbiter bound (n+1 cycles) and per-core timing independence. diff --git a/dv/formal/rabbit5/Makefile b/dv/formal/rabbit5/Makefile new file mode 100644 index 0000000..e9f662d --- /dev/null +++ b/dv/formal/rabbit5/Makefile @@ -0,0 +1,64 @@ +# Run riscv-formal on rabbit5. +# make riscv-formal checks + rabbit5 timing properties +# make riscv-formal only the riscv-formal checks (parallel) +# make timing only the timing properties +# make generate only (re)generate the .sby files +# make check C=insn_add_ch0 run one check by name +REPO ?= $(abspath ../../..) +RF_SRC := $(REPO)/third_party/riscv-formal +RTL := $(REPO)/rtl/cores/rabbit5 +BUILD := build +# genchecks.py expects /cores//, so build a small mirror +MIRROR := $(BUILD)/riscv-formal +CORE_DIR := $(MIRROR)/cores/rabbit5 +JOBS ?= $(shell nproc) +FLAT := $(BUILD)/rabbit5_flat.v +# slang is built into some Yosys builds and a plugin in others (OSS CAD Suite) +YOSYS_SLANG := $(shell yosys -p 'help read_slang' >/dev/null 2>&1 || echo -m slang) + +SOURCES := $(addprefix $(RTL)/,rabbit5_pkg.sv rabbit5_decoder.sv rabbit5_alu.sv \ + rabbit5_regfile.sv rabbit5_csr.sv rabbit5_core.sv) + +all: riscv-formal timing + +riscv-formal: generate + $(MAKE) -C $(CORE_DIR)/checks -j$(JOBS) -k + @python3 summary.py $(CORE_DIR)/checks + +# rabbit5's own timing properties (timing/rabbit5_timing_tb.sv) +timing: $(BUILD)/slang_load.ys + cd timing && sby -f timing.sby + +$(BUILD)/slang_load.ys: + @mkdir -p $(BUILD) + @if [ -n "$(YOSYS_SLANG)" ]; then echo "plugin -i slang" > $@; else echo "# slang is built in" > $@; fi + +generate: $(CORE_DIR)/checks/makefile + +# 1. rabbit5 is modern SystemVerilog; riscv-formal reads files with Yosys' +# built-in parser, so convert once with the slang frontend. +$(FLAT): $(SOURCES) + @mkdir -p $(BUILD) + yosys $(YOSYS_SLANG) -q -p "read_slang $(SOURCES) --top rabbit5_core -DSYNTHESIS; \ + hierarchy -top rabbit5_core; proc; flatten; opt_clean; \ + write_verilog -noattr $@" + +# 2. mirror + config, 3. generate one .sby per check +$(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv + @mkdir -p $(MIRROR) $(CORE_DIR) + cp $(FLAT) $(CORE_DIR)/ + ln -sfn $(RF_SRC)/checks $(MIRROR)/checks + ln -sfn $(RF_SRC)/insns $(MIRROR)/insns + cp checks.cfg wrapper.sv $(CORE_DIR)/ + rm -rf $(CORE_DIR)/checks + cd $(CORE_DIR) && python3 ../../checks/genchecks.py + +# run a single check, e.g. make check C=insn_add_ch0 +check: generate + $(MAKE) -C $(CORE_DIR)/checks $(C) + @cat $(CORE_DIR)/checks/$(C)/status + +clean: + rm -rf $(BUILD) timing/timing_bmc timing/timing_cover timing/timing + +.PHONY: all riscv-formal timing generate check clean diff --git a/dv/formal/rabbit5/checks.cfg b/dv/formal/rabbit5/checks.cfg new file mode 100644 index 0000000..37effc0 --- /dev/null +++ b/dv/formal/rabbit5/checks.cfg @@ -0,0 +1,35 @@ +# riscv-formal configuration for rabbit5 (see dv/formal/README.md) +# +# [depth] columns: [start] [step to check at] (BMC cycles) +# rabbit5 needs 5 cycles after reset for the first instruction to retire. + +[options] +isa rv32i + +[depth] +insn 12 +reg 10 15 +pc_fwd 10 15 +pc_bwd 10 15 +unique 1 10 15 +causal 10 15 +liveness 1 10 20 +ill 12 +cover 1 20 + +[sort] +reg_ch0 + +[defines] +`define RISCV_FORMAL_ALIGNED_MEM + +[verilog-files] +@basedir@/cores/@core@/wrapper.sv +@basedir@/cores/@core@/rabbit5_flat.v + +[cover] +# Non-vacuity at cycle 20: full throughput (16 retired: 5..20) and a trap. +# The slowest case (6 retired) and the exact timing model are proven in +# timing/rabbit5_timing_tb.sv, where the solver finds them in seconds. +always @* if (!reset) cover (channel[0].cnt_insns == 16); +always @* if (!reset) cover (channel[0].valid && channel[0].trap); diff --git a/dv/formal/rabbit5/summary.py b/dv/formal/rabbit5/summary.py new file mode 100644 index 0000000..14352ed --- /dev/null +++ b/dv/formal/rabbit5/summary.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python3 +"""Print PASS/FAIL per riscv-formal check and exit non-zero on any failure.""" +import sys +from pathlib import Path + +root = Path(sys.argv[1]) +results = {} +for d in sorted(p for p in root.iterdir() if p.is_dir()): + status = d / "status" + results[d.name] = status.read_text().split()[0] if status.exists() else "MISSING" + +bad = {k: v for k, v in results.items() if v not in ("PASS",)} +print(f"riscv-formal: {len(results) - len(bad)}/{len(results)} checks PASS") +for k, v in bad.items(): + print(f" {v:8s} {k} (trace: {root / k / 'engine_0'})") +sys.exit(1 if bad else 0) diff --git a/dv/formal/rabbit5/timing/rabbit5_timing_tb.sv b/dv/formal/rabbit5/timing/rabbit5_timing_tb.sv new file mode 100644 index 0000000..3c638b6 --- /dev/null +++ b/dv/formal/rabbit5/timing/rabbit5_timing_tb.sv @@ -0,0 +1,167 @@ +// ============================================================================= +// rabbit5 timing properties (beyond riscv-formal) +// ============================================================================= +// riscv-formal proves WHAT each instruction computes. These properties prove +// WHEN: they turn the "TIMING RULES" comment in rabbit5_core.sv into checked +// facts. They look only at the RVFI trace and the memory bus, so they treat the +// core as a black box and can be reused for any future rabbit core. +// +// T1 exact timing model: the gap between two consecutive retirements is +// 3 cycles if the earlier instruction changed control flow +// (taken branch, JAL, JALR, MRET, trap) [rule R3] +// 2 cycles if the later one reads the register the earlier +// one loaded (load-use) [rule R2] +// 1 cycle otherwise [rule R1] +// T2 the first instruction retires exactly FIRST_RETIRE cycles after reset +// T3 a data-memory request happens exactly one cycle before the instruction +// that made it retires, and never at any other time [rule R4] +// +// The solver picks ANY instruction word and ANY load data every cycle. +// +// Ideas for properties to add next (robotics / real-time): +// - bounded interrupt latency, once interrupts exist (M2) +// - for the dual core (M4): core 0's T1 gaps never depend on core 1 +// ============================================================================= +module rabbit5_timing_tb ( + input logic clk +); + localparam int FIRST_RETIRE = 5; + + // ---- free inputs: any instruction, any load data, every cycle ------------- + (* anyseq *) logic [31:0] instr_rdata; + (* anyseq *) logic [31:0] data_rdata; + + // ---- reset for exactly the first cycle ------------------------------------- + logic rst_n = 1'b0; + always_ff @(posedge clk) rst_n <= 1'b1; + + logic data_req; + logic rvfi_valid, rvfi_trap; + logic [31:0] rvfi_insn, rvfi_rs1_rdata, rvfi_rs2_rdata; + logic [4:0] rvfi_rs1_addr, rvfi_rs2_addr, rvfi_rd_addr; + logic [3:0] rvfi_mem_rmask, rvfi_mem_wmask; + + rabbit5_core dut ( + .clk_i(clk), .rst_ni(rst_n), .fetch_enable_i(1'b1), + .instr_req_o(), .instr_gnt_i(1'b1), .instr_rvalid_i(1'b1), + .instr_addr_o(), .instr_rdata_i(instr_rdata), + .data_req_o(data_req), .data_gnt_i(1'b1), .data_rvalid_i(1'b1), + .data_we_o(), .data_be_o(), .data_addr_o(), .data_wdata_o(), + .data_rdata_i(data_rdata), + .irq_i(32'b0), + .rvfi_valid(rvfi_valid), .rvfi_order(), .rvfi_insn(rvfi_insn), + .rvfi_trap(rvfi_trap), .rvfi_halt(), .rvfi_intr(), .rvfi_mode(), .rvfi_ixl(), + .rvfi_rs1_addr(rvfi_rs1_addr), .rvfi_rs2_addr(rvfi_rs2_addr), + .rvfi_rs1_rdata(rvfi_rs1_rdata), .rvfi_rs2_rdata(rvfi_rs2_rdata), + .rvfi_rd_addr(rvfi_rd_addr), .rvfi_rd_wdata(), + .rvfi_pc_rdata(), .rvfi_pc_wdata(), .rvfi_mem_addr(), + .rvfi_mem_rmask(rvfi_mem_rmask), .rvfi_mem_wmask(rvfi_mem_wmask), + .rvfi_mem_rdata(), .rvfi_mem_wdata() + ); + + // ---- classify the instruction that retires now ------------------------------ + // (the ISA-level meaning only; nothing about how rabbit5 is built) + logic [6:0] opcode; + logic [2:0] funct3; + assign opcode = rvfi_insn[6:0]; + assign funct3 = rvfi_insn[14:12]; + + logic branch_taken; + always_comb begin + case (funct3) + 3'b000 : branch_taken = (rvfi_rs1_rdata == rvfi_rs2_rdata); + 3'b001 : branch_taken = (rvfi_rs1_rdata != rvfi_rs2_rdata); + 3'b100 : branch_taken = ($signed(rvfi_rs1_rdata) < $signed(rvfi_rs2_rdata)); + 3'b101 : branch_taken = ($signed(rvfi_rs1_rdata) >= $signed(rvfi_rs2_rdata)); + 3'b110 : branch_taken = (rvfi_rs1_rdata < rvfi_rs2_rdata); + 3'b111 : branch_taken = (rvfi_rs1_rdata >= rvfi_rs2_rdata); + default: branch_taken = 1'b0; + endcase + end + + logic changes_flow, is_load; + assign changes_flow = rvfi_trap + || opcode == 7'b1101111 // JAL + || opcode == 7'b1100111 // JALR + || rvfi_insn == 32'h3020_0073 // MRET + || (opcode == 7'b1100011 && branch_taken); // taken branch + assign is_load = (opcode == 7'b0000011) && !rvfi_trap; + + // ---- remember the previous retirement -------------------------------------------- + logic seen_one; // at least one instruction has retired + logic prev_flow; // previous instruction changed control flow + logic prev_load; // previous instruction was a load ... + logic [4:0] prev_rd; // ... into this register (0 = none) + int gap; // cycles since the previous retirement + int cycle; // cycles since reset was released + + always_ff @(posedge clk) begin + if (!rst_n) begin + seen_one <= 1'b0; + gap <= 0; + cycle <= 0; + end else begin + cycle <= cycle + 1; + if (rvfi_valid) begin + seen_one <= 1'b1; + prev_flow <= changes_flow; + prev_load <= is_load; + prev_rd <= rvfi_rd_addr; + gap <= 1; + end else begin + gap <= gap + 1; + end + end + end + + logic load_use; + assign load_use = prev_load && prev_rd != 5'd0 && + (rvfi_rs1_addr == prev_rd || rvfi_rs2_addr == prev_rd); + + int expected_gap; + assign expected_gap = prev_flow ? 3 : (load_use ? 2 : 1); + + // ---- T1, T2 ------------------------------------------------------------------------ + always_comb begin + if (rst_n && rvfi_valid) begin + if (seen_one) assert (gap == expected_gap); // T1 + else assert (cycle == FIRST_RETIRE - 1); // T2 (cycle counts from 0) + end + if (rst_n && !seen_one) assert (cycle < FIRST_RETIRE); // T2: nothing is late + end + + // ---- T3: memory is used exactly one cycle before retirement --------------------------- + logic data_req_q = 1'b0; + always_ff @(posedge clk) data_req_q <= data_req; + + always_comb begin + if (rst_n) assert (data_req_q == (rvfi_valid && (rvfi_mem_rmask != 0 || rvfi_mem_wmask != 0))); + end + + // ---- throughput bounds ------------------------------------------------------------------ + // From T1 + T2: after the first retirement (cycle 4), every 1..3 cycles one + // more instruction retires. So at cycle 19 between 6 and 16 have retired. + // Both extremes must be reachable (covers below). + int retired; + always_ff @(posedge clk) begin + if (!rst_n) retired <= 0; + else if (rvfi_valid) retired <= retired + 1; + end + logic [31:0] retired_now; // including an instruction retiring this cycle + assign retired_now = retired + (rvfi_valid ? 1 : 0); + + // ---- non-vacuity: every case of T1 must really happen ------------------------------------ + always_comb begin + if (rst_n && cycle == 19) begin + cover (retired_now == 6); // slowest possible: every instruction redirects + cover (retired_now == 16); // fastest possible: no bubbles at all + end + if (rst_n && rvfi_valid && seen_one) begin + cover (gap == 1); + cover (gap == 2); + cover (gap == 3); + cover (gap == 2 && load_use); + cover (gap == 3 && rvfi_trap); + end + end +endmodule diff --git a/dv/formal/rabbit5/timing/timing.sby b/dv/formal/rabbit5/timing/timing.sby new file mode 100644 index 0000000..4db2862 --- /dev/null +++ b/dv/formal/rabbit5/timing/timing.sby @@ -0,0 +1,29 @@ +# rabbit5 timing properties. Run from dv/formal/rabbit5: make timing +# (the Makefile writes ../build/slang_load.ys, which loads the slang plugin +# only on Yosys builds where it is not built in) +[tasks] +bmc +cover + +[options] +bmc: mode bmc +cover: mode cover +depth 24 + +[engines] +smtbmc boolector + +[script] +script slang_load.ys +read_slang rabbit5_pkg.sv rabbit5_decoder.sv rabbit5_alu.sv rabbit5_regfile.sv rabbit5_csr.sv rabbit5_core.sv rabbit5_timing_tb.sv --top rabbit5_timing_tb -DSYNTHESIS +prep -top rabbit5_timing_tb + +[files] +../build/slang_load.ys +../../../../rtl/cores/rabbit5/rabbit5_pkg.sv +../../../../rtl/cores/rabbit5/rabbit5_decoder.sv +../../../../rtl/cores/rabbit5/rabbit5_alu.sv +../../../../rtl/cores/rabbit5/rabbit5_regfile.sv +../../../../rtl/cores/rabbit5/rabbit5_csr.sv +../../../../rtl/cores/rabbit5/rabbit5_core.sv +rabbit5_timing_tb.sv diff --git a/dv/formal/rabbit5/wrapper.sv b/dv/formal/rabbit5/wrapper.sv new file mode 100644 index 0000000..0b58cb8 --- /dev/null +++ b/dv/formal/rabbit5/wrapper.sv @@ -0,0 +1,50 @@ +// riscv-formal wrapper for rabbit5. +// +// The solver may choose ANY instruction word and ANY load data in every +// cycle (`rvformal_rand_reg). That is what makes the checks exhaustive: every +// instruction sequence up to the check depth is covered, not just programs we +// thought of. +// +// Memory contract (rabbit5 rule R4): requests are granted immediately and the +// answer comes one cycle later. We model exactly that and nothing more. +module rvfi_wrapper ( + input clock, + input reset, + `RVFI_OUTPUTS +); + (* keep *) `rvformal_rand_reg [31:0] instr_rdata; + (* keep *) `rvformal_rand_reg [31:0] data_rdata; + + (* keep *) wire instr_req; + (* keep *) wire [31:0] instr_addr; + (* keep *) wire data_req; + (* keep *) wire data_we; + (* keep *) wire [ 3:0] data_be; + (* keep *) wire [31:0] data_addr; + (* keep *) wire [31:0] data_wdata; + + rabbit5_core uut ( + .clk_i (clock), + .rst_ni (!reset), + .fetch_enable_i (1'b1), + + .instr_req_o (instr_req), + .instr_gnt_i (1'b1), + .instr_rvalid_i (1'b1), + .instr_addr_o (instr_addr), + .instr_rdata_i (instr_rdata), + + .data_req_o (data_req), + .data_gnt_i (1'b1), + .data_rvalid_i (1'b1), + .data_we_o (data_we), + .data_be_o (data_be), + .data_addr_o (data_addr), + .data_wdata_o (data_wdata), + .data_rdata_i (data_rdata), + + .irq_i (32'b0), + + `RVFI_CONN32 + ); +endmodule diff --git a/rtl/cores/README.md b/rtl/cores/README.md index e7e45e8..bd36c7b 100644 --- a/rtl/cores/README.md +++ b/rtl/cores/README.md @@ -49,9 +49,10 @@ adapter, in `rtl/soc/`. | `cv32e40p/` | OpenHW CV32E40P v1.8.3 (RV32IMC, 4-stage) | **working** | Baseline for Y1 | | `ibex/` | lowRISC Ibex | planned | Same OBI-like bus, 2/3-stage; good for area comparison | | `cv32e40x/` | OpenHW CV32E40X | planned | Brings CV-X-IF for the vector/NN coprocessor | -| `rabbit5/` | Our own 5-stage, timing-predictable core | Y1 H2 | Grows out of `verilog-riscV32I-machine` | +| `rabbit5/` | Our own 5-stage, timing-predictable RV32I core | **working (v0)** | riscv-formal 45/45, timing properties, GLS smoke — see its README | The contract will grow (v1) with an optional **coprocessor port** (CV-X-IF style) and an optional **RVFI trace port** for lockstep checking against Spike/Sail. +(rabbit5 already has RVFI on `rabbit5_core`; the adapter leaves it unconnected.) Cores that lack a feature tie the outputs off; the SoC checks capabilities at elaboration time. diff --git a/rtl/cores/rabbit5/README.md b/rtl/cores/rabbit5/README.md new file mode 100644 index 0000000..23568ea --- /dev/null +++ b/rtl/cores/rabbit5/README.md @@ -0,0 +1,86 @@ +# rabbit5 — our own timing-predictable RV32I core (v0) + +A classic 5-stage, single-issue, in-order RV32I pipeline written to be **read, +reviewed and modified**, with one research goal: *every instruction's timing is +known in advance and proven*. Plugs into the SoC through the same `rabbit_cpu` +contract as CV32E40P, so both run the same firmware and tests. + +``` +IF ──► ID ──► EX ──► MEM ──► WB + │ │ │ └ load data arrives, register write, RVFI report + │ │ └ data memory request + │ └ ALU, branch decision, CSRs, traps (commit point) + └ decode, register read, load-use detection +``` + +## Status (2026-11-06) + +| What | Result | Command | +|---|---|---| +| `hello` firmware in the SoC | PASS, 3958 cycles (CV32E40P: 3450, it has HW mul/div) | `make soc-sim CORE=rabbit5` | +| riscv-formal (37 instructions + reg, pc_fwd, pc_bwd, causal, unique, liveness, ill, cover) | **45/45 PASS** | `make formal` | +| Timing properties T1–T3 (ours, beyond riscv-formal) | PASS (BMC depth 24) + all covers reached | `make formal` | +| Gate-level smoke test (Yosys generic gates) | PASS, **same 3958 cycles** as RTL | `make gls-smoke CORE=rabbit5` | +| Verilator `-Wall` lint | clean | `make lint CORE=rabbit5` | +| Size (Yosys generic synthesis, core + adapter) | ≈ 10.9 k cells | `make gls-netlist CORE=rabbit5` | + +Whole formal suite: ~35 s on a 22-core machine. + +## Reading order (≈ 1,000 lines of RTL, comments included) + +| # | File | Lines | What to understand | +|---|---|---|---| +| 1 | `rabbit5_pkg.sv` | ~110 | opcodes, ALU ops, the `decoded_t` struct, CSR numbers | +| 2 | `rabbit5_alu.sv` | ~30 | nothing surprising — good warm-up | +| 3 | `rabbit5_decoder.sv` | ~200 | 32 bits → `decoded_t`; what counts as *illegal* | +| 4 | `rabbit5_regfile.sv` | ~35 | why the write-first bypass removes one hazard | +| 5 | `rabbit5_core.sv` | ~500 | **the pipeline** — start with the TIMING RULES header | +| 6 | `rabbit5_csr.sv` | ~130 | machine-mode CSRs, trap entry, MRET | +| 7 | `../../../dv/formal/rabbit5/timing/rabbit5_timing_tb.sv` | ~170 | the timing properties T1–T3 | +| 8 | `../../../dv/formal/rabbit5/wrapper.sv`, `checks.cfg` | | how riscv-formal sees the core | + +## The timing model (rules R1–R5, in `rabbit5_core.sv`) + +1. **R1** one instruction retires per cycle, except: +2. **R2** load-use: 1 bubble if an instruction reads the register loaded by the instruction just before it; +3. **R3** every redirect (taken branch, JAL, JALR, MRET, trap) is decided in EX: exactly 2 bubbles, no prediction; +4. **R4** memory grants immediately and answers after exactly 1 cycle (scratchpad assumption); +5. **R5** nothing else stalls. + +**Consequence (proven as T1):** the time between two consecutive retirements is +1, 2 or 3 cycles and depends only on those two instructions. For a straight-line +or loop path you can compute the cycle count by hand — that is what makes WCET +analysis trivial for this core. + +## Review checklist — what is worth a second pair of eyes + +Design choices you may want to change: +- [ ] **Branches resolved in EX (2-cycle penalty).** Resolving JAL in ID would save 1 cycle on every call/jump but makes the timing rule depend on instruction type in two places. Trade-off: speed vs. simplicity of the timing model. +- [ ] **No branch prediction** — deliberate (predictors make timing history-dependent). +- [ ] **Load data arrives in WB, forwarded to EX from WB** — keeps the load-use penalty at 1. +- [ ] **All pipeline registers have an asynchronous reset** — costs area, removes X in simulation/GLS. +- [ ] **`minstret` counts at EX (commit point)**, so a CSR read sees all older instructions. +- [ ] Misaligned loads/stores **trap** (cause 4/6) rather than being split into two accesses. + +Things to verify yourself (good first exercises): +- [ ] Draw the pipeline diagram for `lw x1,0(x2); add x3,x1,x1` and check it against a waveform (`make soc-waves CORE=rabbit5`). +- [ ] Find where `stall` and `redirect` interact (`assign stall = load_use && !redirect`) and convince yourself why the order matters. +- [ ] Break something on purpose (e.g. swap the MEM/WB priority in `forward()`) and watch which formal check fails. We did this: only **`reg_ch0`** catches it — all 37 instruction checks still pass, because each instruction is correct *for the operands it was given*. + +## Known limitations of v0 + +| Limitation | Planned | +|---|---| +| No interrupts (`irq_i` ignored), no debug module | M2: timer + external IRQ with a **bounded, proven** entry latency | +| Memory must be zero-wait (R4); no back-pressure | M4: TDM scratchpad arbiter → stall only in MEM (Patmos rule) | +| CSRs are not formally checked (riscv-formal `csrw`/`csrc_*` checks not enabled yet) | M2 | +| BMC proves properties up to a depth (24 cycles timing, 12–20 riscv-formal), not unbounded | try `mode prove` (k-induction) once stable | +| No M/C extensions (software mul/div) | later; a single-cycle multiplier keeps R1 intact | +| Register file not reset (x1..x31 start as X in gate-level sim) | fine for software that initialises registers | + +## Ideas for your own properties (robotics / real time) + +- **Loop timing:** for a given loop body, cycles per iteration is constant — express as "the gap pattern between retirements of a repeated PC sequence is periodic". +- **Interrupt latency (after M2):** from `irq_i` rising to the first handler instruction retiring ≤ K cycles, for all program states. +- **Memory slot predictability (T3 extended):** the data bus is used *only* in the cycle before retirement — the property the TDM arbiter of the dual core will rely on. +- **Dual core (M4):** core 0's T1 gaps are unchanged whatever core 1 executes. diff --git a/rtl/cores/rabbit5/core.mk b/rtl/cores/rabbit5/core.mk new file mode 100644 index 0000000..1f53cc2 --- /dev/null +++ b/rtl/cores/rabbit5/core.mk @@ -0,0 +1,5 @@ +# Per-core build settings, included by the top-level and dv Makefiles. +CORE_MARCH := rv32i_zicsr +CORE_MABI := ilp32 +# Our own RTL: no warning suppressions. +CORE_VERILATOR_FLAGS := diff --git a/rtl/cores/rabbit5/files.f b/rtl/cores/rabbit5/files.f new file mode 100644 index 0000000..0f11a6b --- /dev/null +++ b/rtl/cores/rabbit5/files.f @@ -0,0 +1,8 @@ +// rabbit5 (RV32I, 5-stage) + rabbit_cpu adapter. ${REPO} is expanded by Verilator. +${REPO}/rtl/cores/rabbit5/rabbit5_pkg.sv +${REPO}/rtl/cores/rabbit5/rabbit5_decoder.sv +${REPO}/rtl/cores/rabbit5/rabbit5_alu.sv +${REPO}/rtl/cores/rabbit5/rabbit5_regfile.sv +${REPO}/rtl/cores/rabbit5/rabbit5_csr.sv +${REPO}/rtl/cores/rabbit5/rabbit5_core.sv +${REPO}/rtl/cores/rabbit5/rabbit_cpu.sv diff --git a/rtl/cores/rabbit5/rabbit5_alu.sv b/rtl/cores/rabbit5/rabbit5_alu.sv new file mode 100644 index 0000000..8a0ff51 --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_alu.sv @@ -0,0 +1,30 @@ +// ============================================================================= +// rabbit5_alu — RV32I integer ALU (pure combinational, one cycle) +// ============================================================================= +module rabbit5_alu + import rabbit5_pkg::*; +( + input alu_op_e op_i, + input logic [31:0] a_i, + input logic [31:0] b_i, + output logic [31:0] y_o +); + logic [4:0] shamt; + assign shamt = b_i[4:0]; // RV32I uses only the low 5 bits as shift amount + + always_comb begin + unique case (op_i) + ALU_ADD : y_o = a_i + b_i; + ALU_SUB : y_o = a_i - b_i; + ALU_SLL : y_o = a_i << shamt; + ALU_SRL : y_o = a_i >> shamt; + ALU_SRA : y_o = $unsigned($signed(a_i) >>> shamt); + ALU_SLT : y_o = {31'b0, $signed(a_i) < $signed(b_i)}; + ALU_SLTU: y_o = {31'b0, a_i < b_i}; + ALU_XOR : y_o = a_i ^ b_i; + ALU_OR : y_o = a_i | b_i; + ALU_AND : y_o = a_i & b_i; + default : y_o = 32'b0; + endcase + end +endmodule diff --git a/rtl/cores/rabbit5/rabbit5_core.sv b/rtl/cores/rabbit5/rabbit5_core.sv new file mode 100644 index 0000000..2333640 --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_core.sv @@ -0,0 +1,496 @@ +// ============================================================================= +// rabbit5_core — 5-stage in-order RV32I pipeline (v0, single hart) +// ============================================================================= +// +// cycle: 1 2 3 4 5 6 +// instr A IF ID EX MEM WB +// instr B IF ID EX MEM WB +// +// IF : send pc to instruction memory +// ID : instruction word arrives; decode; read registers; detect load-use +// EX : ALU, branch decision, CSR access, traps <- commit point +// MEM : send load/store to data memory +// WB : load data arrives; write register; report to RVFI +// +// ----------------------------------------------------------------------------- +// TIMING RULES (the whole timing model of v0 — checked in dv/formal/rabbit5/timing) +// ----------------------------------------------------------------------------- +// R1 One instruction retires per cycle, except: +// R2 Load-use: if an instruction reads the register loaded by the load +// directly before it, it waits exactly 1 cycle (1 bubble). +// R3 Redirect: every change of control flow — taken branch, JAL, JALR, +// MRET, any trap — is decided in EX and costs exactly 2 cycles +// (2 bubbles). No branch prediction, so the cost never depends on history. +// R4 Memory must answer in exactly 1 cycle (grant in the request cycle, +// data the next cycle). This is the scratchpad-memory assumption from +// FlexPRET/Patmos; the core never waits on memory. +// R5 Nothing else ever stalls the pipeline. +// +// So the time between two consecutive retirements is 1, 2 (R2) or 3 (R3) +// cycles and depends only on those two instructions. +// ----------------------------------------------------------------------------- +// +// Bus: OBI-style request/grant/rvalid, as in the rabbit_cpu contract. +// Verification port: RVFI (riscv-formal interface), always present; it costs +// nothing in synthesis when left unconnected. +// ============================================================================= +module rabbit5_core + import rabbit5_pkg::*; +#( + parameter logic [31:0] BOOT_ADDR = 32'h0000_0080, + parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000, + parameter logic [31:0] HART_ID = 32'h0000_0000 +) ( + input logic clk_i, + input logic rst_ni, + input logic fetch_enable_i, + + // instruction memory + output logic instr_req_o, + input logic instr_gnt_i, + input logic instr_rvalid_i, + output logic [31:0] instr_addr_o, + input logic [31:0] instr_rdata_i, + + // data memory + output logic data_req_o, + input logic data_gnt_i, + input logic data_rvalid_i, + output logic data_we_o, + output logic [ 3:0] data_be_o, + output logic [31:0] data_addr_o, + output logic [31:0] data_wdata_o, + input logic [31:0] data_rdata_i, + + input logic [31:0] irq_i, // not used in v0 + + // RVFI: one record per retired instruction, valid in its WB cycle + output logic rvfi_valid, + output logic [63:0] rvfi_order, + output logic [31:0] rvfi_insn, + output logic rvfi_trap, + output logic rvfi_halt, + output logic rvfi_intr, + output logic [ 1:0] rvfi_mode, + output logic [ 1:0] rvfi_ixl, + output logic [ 4:0] rvfi_rs1_addr, + output logic [ 4:0] rvfi_rs2_addr, + output logic [31:0] rvfi_rs1_rdata, + output logic [31:0] rvfi_rs2_rdata, + output logic [ 4:0] rvfi_rd_addr, + output logic [31:0] rvfi_rd_wdata, + output logic [31:0] rvfi_pc_rdata, + output logic [31:0] rvfi_pc_wdata, + output logic [31:0] rvfi_mem_addr, + output logic [ 3:0] rvfi_mem_rmask, + output logic [ 3:0] rvfi_mem_wmask, + output logic [31:0] rvfi_mem_rdata, + output logic [31:0] rvfi_mem_wdata +); + + // =========================================================================== + // Pipeline registers. Each struct is "what this stage needs to know". + // =========================================================================== + + // ID/EX + typedef struct packed { + logic valid; + logic [31:0] pc; + logic [31:0] instr; + decoded_t dec; + logic [31:0] rs1_val; // register values read in ID (EX may forward newer ones) + logic [31:0] rs2_val; + } ex_stage_t; + + // EX/MEM and MEM/WB (same content; WB additionally receives load data) + typedef struct packed { + logic valid; + logic [31:0] pc; + logic [31:0] instr; + logic [31:0] next_pc; // where the program goes after this instruction + logic trap; // instruction trapped in EX: no side effects + logic writes_rd; + logic [4:0] rd; + logic [31:0] result; // ALU / link / CSR value (loads: filled in WB) + logic is_load; + logic is_store; + logic [2:0] funct3; // load/store size and sign + logic [31:0] addr; // byte address of the load/store + logic [31:0] store_data; + logic [4:0] rs1_addr; // for RVFI only + logic [4:0] rs2_addr; + logic [31:0] rs1_val; + logic [31:0] rs2_val; + } mem_stage_t; + + logic redirect; // EX changes control flow this cycle + logic [31:0] redirect_pc; + logic stall; // ID must wait one cycle (load-use) + + // =========================================================================== + // IF — instruction fetch + // =========================================================================== + // pc_q is the address requested *this* cycle. The memory answers next + // cycle, when the instruction is in ID (rule R4). + logic [31:0] pc_q; + + assign instr_req_o = fetch_enable_i; + assign instr_addr_o = pc_q; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) pc_q <= BOOT_ADDR; + else if (redirect) pc_q <= redirect_pc; // R3 + else if (stall) pc_q <= pc_q; // R2: ask for the same word again + else if (fetch_enable_i) pc_q <= pc_q + 32'd4; + end + + // =========================================================================== + // ID — decode and register read + // =========================================================================== + // While ID is stalled, the memory is already returning the *next* word, so + // the stalled instruction is kept in a small holding register. + logic id_valid_q; + logic [31:0] id_pc_q; + logic id_hold_q; + logic [31:0] id_hold_instr_q; + logic [31:0] id_instr; + + assign id_instr = id_hold_q ? id_hold_instr_q : instr_rdata_i; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + id_valid_q <= 1'b0; + id_hold_q <= 1'b0; + id_hold_instr_q <= '0; + id_pc_q <= '0; + end else if (redirect) begin // wrong-path instruction: drop it + id_valid_q <= 1'b0; + id_hold_q <= 1'b0; + end else if (stall) begin // keep the same instruction + id_hold_q <= 1'b1; + id_hold_instr_q <= id_instr; + end else begin // take the word requested this cycle + id_valid_q <= fetch_enable_i; + id_hold_q <= 1'b0; + id_pc_q <= pc_q; + end + end + + decoded_t id_dec; + rabbit5_decoder u_decoder (.instr_i(id_instr), .dec_o(id_dec)); + + // Register file: read in ID, written in WB + logic rf_we; + logic [4:0] rf_waddr; + logic [31:0] rf_wdata; + logic [31:0] id_rs1_val, id_rs2_val; + + rabbit5_regfile u_regfile ( + .clk_i, + .raddr_a_i(id_dec.rs1), .rdata_a_o(id_rs1_val), + .raddr_b_i(id_dec.rs2), .rdata_b_o(id_rs2_val), + .we_i(rf_we), .waddr_i(rf_waddr), .wdata_i(rf_wdata) + ); + + // =========================================================================== + // EX — execute (ex_q is the ID/EX pipeline register) + // =========================================================================== + ex_stage_t ex_q; + mem_stage_t mem_q; // EX/MEM + mem_stage_t wb_q; // MEM/WB + logic [31:0] wb_result; + + // Load-use hazard (rule R2): the load is in EX now, its data only exists + // in WB, two cycles from now. Hold the dependent instruction for one cycle. + logic load_use; + assign load_use = id_valid_q && ex_q.valid && ex_q.dec.is_load && ex_q.dec.writes_rd && + ((id_dec.uses_rs1 && id_dec.rs1 == ex_q.dec.rd) || + (id_dec.uses_rs2 && id_dec.rs2 == ex_q.dec.rd)); + assign stall = load_use && !redirect; // a redirect throws the ID instruction away anyway + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) ex_q <= '0; + else if (redirect || stall) ex_q.valid <= 1'b0; // insert a bubble + else begin + ex_q.valid <= id_valid_q; + ex_q.pc <= id_pc_q; + ex_q.instr <= id_instr; + ex_q.dec <= id_dec; + ex_q.rs1_val <= id_rs1_val; + ex_q.rs2_val <= id_rs2_val; + end + end + + // ---- forwarding: use the newest value of a register ----------------------- + // Priority: MEM (younger) over WB (older) over the value read in ID. + // A load in MEM never needs forwarding here: R2 guarantees a bubble. + function automatic logic [31:0] forward(input logic [4:0] r, input logic [31:0] id_val); + if (mem_q.valid && mem_q.writes_rd && !mem_q.is_load && mem_q.rd == r) return mem_q.result; + else if (wb_q.valid && wb_q.writes_rd && wb_q.rd == r) return wb_result; + else return id_val; + endfunction + + logic [31:0] rs1, rs2; + assign rs1 = forward(ex_q.dec.rs1, ex_q.rs1_val); + assign rs2 = forward(ex_q.dec.rs2, ex_q.rs2_val); + + // ---- ALU ------------------------------------------------------------------ + logic [31:0] alu_a, alu_b, alu_y; + always_comb begin + unique case (ex_q.dec.opa) + OPA_RS1: alu_a = rs1; + OPA_PC : alu_a = ex_q.pc; + default: alu_a = 32'b0; + endcase + alu_b = (ex_q.dec.opb == OPB_RS2) ? rs2 : ex_q.dec.imm; + end + + rabbit5_alu u_alu (.op_i(ex_q.dec.alu_op), .a_i(alu_a), .b_i(alu_b), .y_o(alu_y)); + + // ---- branches and jumps ----------------------------------------------------- + logic branch_cond; + always_comb begin + unique case (ex_q.dec.funct3) + 3'b000 : branch_cond = (rs1 == rs2); // BEQ + 3'b001 : branch_cond = (rs1 != rs2); // BNE + 3'b100 : branch_cond = ($signed(rs1) < $signed(rs2)); // BLT + 3'b101 : branch_cond = ($signed(rs1) >= $signed(rs2)); // BGE + 3'b110 : branch_cond = (rs1 < rs2); // BLTU + 3'b111 : branch_cond = (rs1 >= rs2); // BGEU + default: branch_cond = 1'b0; + endcase + end + + logic taken; + logic [31:0] jump_target; + assign taken = ex_q.dec.is_jal || ex_q.dec.is_jalr || (ex_q.dec.is_branch && branch_cond); + assign jump_target = ex_q.dec.is_jalr ? ((rs1 + ex_q.dec.imm) & ~32'd1) + : (ex_q.pc + ex_q.dec.imm); + + // ---- exceptions (all detected here, in EX) ----------------------------------- + logic csr_illegal; + logic target_misaligned, mem_misaligned; + assign target_misaligned = taken && (jump_target[1:0] != 2'b00); + always_comb begin + unique case (ex_q.dec.funct3[1:0]) + 2'b00 : mem_misaligned = 1'b0; // byte + 2'b01 : mem_misaligned = alu_y[0]; // half word + default: mem_misaligned = (alu_y[1:0] != 2'b00); // word + endcase + mem_misaligned = mem_misaligned && (ex_q.dec.is_load || ex_q.dec.is_store); + end + + logic trap; + logic [31:0] trap_cause, trap_tval; + always_comb begin + trap = 1'b1; + trap_tval = 32'b0; + if (ex_q.dec.illegal || csr_illegal) begin trap_cause = CAUSE_ILLEGAL_INSN; trap_tval = ex_q.instr; end + else if (ex_q.dec.is_ecall) trap_cause = CAUSE_ECALL_M; + else if (ex_q.dec.is_ebreak) trap_cause = CAUSE_BREAKPOINT; + else if (target_misaligned) begin trap_cause = CAUSE_INSN_MISALIGNED; trap_tval = jump_target; end + else if (mem_misaligned) begin + trap_cause = ex_q.dec.is_load ? CAUSE_LOAD_MISALIGNED : CAUSE_STORE_MISALIGNED; + trap_tval = alu_y; + end + else begin trap = 1'b0; trap_cause = 32'b0; end + trap = trap && ex_q.valid; + end + + // ---- CSRs ------------------------------------------------------------------- + logic [31:0] csr_rdata, mtvec, mepc; + logic csr_write_req; + // CSRRW(I) always writes; CSRRS/CSRRC(I) write only if the rs1 field is not 0 + assign csr_write_req = (ex_q.dec.funct3[1:0] == 2'b01) || (ex_q.dec.rs1 != 5'd0); + + rabbit5_csr #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_csr ( + .clk_i, .rst_ni, + .csr_valid_i (ex_q.valid && ex_q.dec.is_csr), + .csr_addr_i (ex_q.instr[31:20]), + .csr_op_i (ex_q.dec.funct3[1:0]), + .csr_write_i (csr_write_req), + .csr_src_i (ex_q.dec.funct3[2] ? ex_q.dec.imm : rs1), + .csr_rdata_o (csr_rdata), + .csr_illegal_o(csr_illegal), + .trap_i (trap), + .trap_cause_i (trap_cause), + .trap_pc_i (ex_q.pc), + .trap_tval_i (trap_tval), + .mret_i (ex_q.valid && ex_q.dec.is_mret), + .instret_i (ex_q.valid && !trap), + .mtvec_o (mtvec), + .mepc_o (mepc) + ); + + // ---- next pc and redirect (rule R3) ------------------------------------------- + logic [31:0] next_pc; + always_comb begin + if (trap) next_pc = mtvec; + else if (ex_q.dec.is_mret) next_pc = mepc; + else if (taken) next_pc = jump_target; + else next_pc = ex_q.pc + 32'd4; + end + assign redirect = ex_q.valid && (trap || ex_q.dec.is_mret || taken); + assign redirect_pc = next_pc; + + // ---- EX result ------------------------------------------------------------------ + logic [31:0] ex_result; + always_comb begin + unique case (ex_q.dec.res) + RES_PC4: ex_result = ex_q.pc + 32'd4; + RES_CSR: ex_result = csr_rdata; + default: ex_result = alu_y; + endcase + end + + // ---- EX/MEM register -------------------------------------------------------------- + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) mem_q <= '0; + else begin + mem_q.valid <= ex_q.valid; + mem_q.pc <= ex_q.pc; + mem_q.instr <= ex_q.instr; + mem_q.next_pc <= next_pc; + mem_q.trap <= trap; + mem_q.writes_rd <= ex_q.dec.writes_rd && !trap; // a trap has no side effects + mem_q.rd <= ex_q.dec.rd; + mem_q.result <= ex_result; + mem_q.is_load <= ex_q.dec.is_load && !trap; + mem_q.is_store <= ex_q.dec.is_store && !trap; + mem_q.funct3 <= ex_q.dec.funct3; + mem_q.addr <= alu_y; + mem_q.store_data <= rs2; + mem_q.rs1_addr <= ex_q.dec.uses_rs1 ? ex_q.dec.rs1 : 5'd0; + mem_q.rs2_addr <= ex_q.dec.uses_rs2 ? ex_q.dec.rs2 : 5'd0; + mem_q.rs1_val <= ex_q.dec.uses_rs1 ? rs1 : 32'd0; + mem_q.rs2_val <= ex_q.dec.uses_rs2 ? rs2 : 32'd0; + end + end + + // =========================================================================== + // MEM — issue the data access (answer arrives in WB, rule R4) + // =========================================================================== + // Byte enables for the 4 bytes of the addressed word + function automatic logic [3:0] byte_mask(input logic [1:0] size, input logic [1:0] offset); + unique case (size) + 2'b00 : return 4'b0001 << offset; // byte + 2'b01 : return 4'b0011 << offset; // half word + default: return 4'b1111; // word + endcase + endfunction + + logic [3:0] mem_mask; + assign mem_mask = byte_mask(mem_q.funct3[1:0], mem_q.addr[1:0]); + + assign data_req_o = mem_q.valid && (mem_q.is_load || mem_q.is_store); + assign data_we_o = mem_q.is_store; + assign data_addr_o = {mem_q.addr[31:2], 2'b00}; + assign data_be_o = mem_mask; + // replicate the store data so each byte lane carries the right byte + always_comb begin + unique case (mem_q.funct3[1:0]) + 2'b00 : data_wdata_o = {4{mem_q.store_data[7:0]}}; + 2'b01 : data_wdata_o = {2{mem_q.store_data[15:0]}}; + default: data_wdata_o = mem_q.store_data; + endcase + end + + // ---- MEM/WB register ---------------------------------------------------------------- + logic [3:0] wb_mask; + logic [31:0] wb_mem_wdata; + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + wb_q <= '0; + wb_mask <= '0; + wb_mem_wdata <= '0; + end else begin + wb_q.valid <= mem_q.valid; + wb_q.pc <= mem_q.pc; + wb_q.instr <= mem_q.instr; + wb_q.next_pc <= mem_q.next_pc; + wb_q.trap <= mem_q.trap; + wb_q.writes_rd <= mem_q.writes_rd; + wb_q.rd <= mem_q.rd; + wb_q.result <= mem_q.result; + wb_q.is_load <= mem_q.is_load; + wb_q.is_store <= mem_q.is_store; + wb_q.funct3 <= mem_q.funct3; + wb_q.addr <= mem_q.addr; + wb_q.store_data <= mem_q.store_data; + wb_q.rs1_addr <= mem_q.rs1_addr; + wb_q.rs2_addr <= mem_q.rs2_addr; + wb_q.rs1_val <= mem_q.rs1_val; + wb_q.rs2_val <= mem_q.rs2_val; + wb_mask <= mem_mask; + wb_mem_wdata <= data_wdata_o; + end + end + + // =========================================================================== + // WB — load data arrives, write the register file + // =========================================================================== + logic [31:0] load_shifted, load_value; + assign load_shifted = data_rdata_i >> {wb_q.addr[1:0], 3'b000}; + always_comb begin + unique case (wb_q.funct3) + 3'b000 : load_value = {{24{load_shifted[7]}}, load_shifted[7:0]}; // LB + 3'b001 : load_value = {{16{load_shifted[15]}}, load_shifted[15:0]}; // LH + 3'b100 : load_value = {24'b0, load_shifted[7:0]}; // LBU + 3'b101 : load_value = {16'b0, load_shifted[15:0]}; // LHU + default: load_value = load_shifted; // LW + endcase + end + + assign wb_result = wb_q.is_load ? load_value : wb_q.result; + assign rf_we = wb_q.valid && wb_q.writes_rd; + assign rf_waddr = wb_q.rd; + assign rf_wdata = wb_result; + + // =========================================================================== + // RVFI — report each retired instruction to the formal checkers + // =========================================================================== + logic [63:0] order_q; + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) order_q <= '0; + else if (wb_q.valid) order_q <= order_q + 64'd1; + end + + assign rvfi_valid = wb_q.valid; + assign rvfi_order = order_q; + assign rvfi_insn = wb_q.instr; + assign rvfi_trap = wb_q.trap; + assign rvfi_halt = 1'b0; + assign rvfi_intr = 1'b0; + assign rvfi_mode = 2'd3; // machine mode + assign rvfi_ixl = 2'd1; // 32-bit + assign rvfi_rs1_addr = wb_q.rs1_addr; + assign rvfi_rs2_addr = wb_q.rs2_addr; + assign rvfi_rs1_rdata = wb_q.rs1_val; + assign rvfi_rs2_rdata = wb_q.rs2_val; + assign rvfi_rd_addr = wb_q.writes_rd ? wb_q.rd : 5'd0; + assign rvfi_rd_wdata = wb_q.writes_rd ? wb_result : 32'd0; + assign rvfi_pc_rdata = wb_q.pc; + assign rvfi_pc_wdata = wb_q.next_pc; + assign rvfi_mem_addr = {wb_q.addr[31:2], 2'b00}; + assign rvfi_mem_rmask = wb_q.is_load ? wb_mask : 4'b0; + assign rvfi_mem_wmask = wb_q.is_store ? wb_mask : 4'b0; + assign rvfi_mem_rdata = data_rdata_i; + assign rvfi_mem_wdata = wb_q.is_store ? wb_mem_wdata : 32'd0; + + // =========================================================================== + // Simulation-only check of rule R4 (the memory contract) + // =========================================================================== +`ifndef SYNTHESIS + always_ff @(posedge clk_i or negedge rst_ni) begin + if (rst_ni) begin + if (instr_req_o && !instr_gnt_i) $error("rabbit5: instruction memory must grant immediately (rule R4)"); + if (data_req_o && !data_gnt_i) $error("rabbit5: data memory must grant immediately (rule R4)"); + end + end +`endif + + // Inputs that v0 does not use (kept so the port list matches rabbit_cpu) + logic unused; + assign unused = ^{instr_rvalid_i, data_rvalid_i, irq_i, wb_q.store_data}; + +endmodule diff --git a/rtl/cores/rabbit5/rabbit5_csr.sv b/rtl/cores/rabbit5/rabbit5_csr.sv new file mode 100644 index 0000000..9328db2 --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_csr.sv @@ -0,0 +1,133 @@ +// ============================================================================= +// rabbit5_csr — machine-mode CSRs and trap state (v0: no interrupts) +// ============================================================================= +// All CSR reads/writes and all trap bookkeeping happen for the instruction in +// EX. EX is the "commit point": nothing after EX can trap, so an instruction +// that leaves EX without a trap is guaranteed to retire. +// +// Implemented: mstatus (MIE, MPIE; MPP fixed to M), misa, mtvec (direct mode), +// mscratch, mepc, mcause, mtval, mcycle[h], minstret[h], mhartid. +// Any other address -> illegal instruction (reported back to EX). +// ============================================================================= +module rabbit5_csr + import rabbit5_pkg::*; +#( + parameter logic [31:0] MTVEC_RESET = 32'h0, + parameter logic [31:0] HART_ID = 32'h0 +) ( + input logic clk_i, + input logic rst_ni, + + // CSR instruction in EX + input logic csr_valid_i, // a CSR instruction is executing (and not trapping for another reason) + input logic [11:0] csr_addr_i, + input logic [1:0] csr_op_i, // funct3[1:0]: 01 = write, 10 = set, 11 = clear + input logic csr_write_i, // the instruction asks to write (RS/RC with x0/0 do not) + input logic [31:0] csr_src_i, // rs1 value or zero-extended immediate + output logic [31:0] csr_rdata_o, // old value -> rd + output logic csr_illegal_o, // unknown CSR, or write to a read-only CSR + + // Trap / return from trap + input logic trap_i, + input logic [31:0] trap_cause_i, + input logic [31:0] trap_pc_i, + input logic [31:0] trap_tval_i, + input logic mret_i, + + // Counting + input logic instret_i, // an instruction committed in EX this cycle + + output logic [31:0] mtvec_o, + output logic [31:0] mepc_o +); + logic mie_q, mpie_q; + logic [31:0] mtvec_q, mscratch_q, mepc_q, mcause_q, mtval_q; + logic [63:0] mcycle_q, minstret_q; + + // ---- read side ------------------------------------------------------------ + logic known; + always_comb begin + known = 1'b1; + csr_rdata_o = 32'b0; + unique case (csr_addr_i) + CSR_MSTATUS : csr_rdata_o = {19'b0, 2'b11, 3'b0, mpie_q, 3'b0, mie_q, 3'b0}; + CSR_MISA : csr_rdata_o = MISA_VALUE; + CSR_MTVEC : csr_rdata_o = mtvec_q; + CSR_MSCRATCH : csr_rdata_o = mscratch_q; + CSR_MEPC : csr_rdata_o = mepc_q; + CSR_MCAUSE : csr_rdata_o = mcause_q; + CSR_MTVAL : csr_rdata_o = mtval_q; + CSR_MCYCLE : csr_rdata_o = mcycle_q[31:0]; + CSR_MCYCLEH : csr_rdata_o = mcycle_q[63:32]; + CSR_MINSTRET : csr_rdata_o = minstret_q[31:0]; + CSR_MINSTRETH: csr_rdata_o = minstret_q[63:32]; + CSR_MHARTID : csr_rdata_o = HART_ID; + default : known = 1'b0; + endcase + end + + // CSR addresses 0xCxx..0xFxx (top two bits = 11) are read-only by definition. + logic read_only; + assign read_only = (csr_addr_i[11:10] == 2'b11); + assign csr_illegal_o = csr_valid_i && (!known || (read_only && csr_write_i)); + + // ---- write side ------------------------------------------------------------- + logic [31:0] wdata; + always_comb begin + unique case (csr_op_i) + 2'b01 : wdata = csr_src_i; // CSRRW(I) + 2'b10 : wdata = csr_rdata_o | csr_src_i; // CSRRS(I) + 2'b11 : wdata = csr_rdata_o & ~csr_src_i; // CSRRC(I) + default: wdata = csr_rdata_o; + endcase + end + + logic we; + assign we = csr_valid_i && csr_write_i && !csr_illegal_o; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + mie_q <= 1'b0; + mpie_q <= 1'b0; + mtvec_q <= {MTVEC_RESET[31:2], 2'b00}; + mscratch_q <= '0; + mepc_q <= '0; + mcause_q <= '0; + mtval_q <= '0; + mcycle_q <= '0; + minstret_q <= '0; + end else begin + // free-running counters (an explicit write below takes priority) + mcycle_q <= mcycle_q + 64'd1; + if (instret_i) minstret_q <= minstret_q + 64'd1; + + if (trap_i) begin + mepc_q <= trap_pc_i; + mcause_q <= trap_cause_i; + mtval_q <= trap_tval_i; + mpie_q <= mie_q; + mie_q <= 1'b0; + end else if (mret_i) begin + mie_q <= mpie_q; + mpie_q <= 1'b1; + end else if (we) begin + unique case (csr_addr_i) + CSR_MSTATUS : begin mie_q <= wdata[3]; mpie_q <= wdata[7]; end + CSR_MTVEC : mtvec_q <= {wdata[31:2], 2'b00}; // direct mode only + CSR_MSCRATCH : mscratch_q <= wdata; + CSR_MEPC : mepc_q <= {wdata[31:2], 2'b00}; // IALIGN = 32 + CSR_MCAUSE : mcause_q <= wdata; + CSR_MTVAL : mtval_q <= wdata; + CSR_MCYCLE : mcycle_q[31:0] <= wdata; + CSR_MCYCLEH : mcycle_q[63:32] <= wdata; + CSR_MINSTRET : minstret_q[31:0] <= wdata; + CSR_MINSTRETH: minstret_q[63:32] <= wdata; + default : ; // misa, mhartid: writes ignored / read-only + endcase + end + end + end + + assign mtvec_o = mtvec_q; + assign mepc_o = mepc_q; +endmodule diff --git a/rtl/cores/rabbit5/rabbit5_decoder.sv b/rtl/cores/rabbit5/rabbit5_decoder.sv new file mode 100644 index 0000000..c5e52c8 --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_decoder.sv @@ -0,0 +1,198 @@ +// ============================================================================= +// rabbit5_decoder — instruction bits -> decoded_t (pure combinational) +// ============================================================================= +// Supported: all of RV32I, plus FENCE and WFI (both executed as no-ops), +// ECALL, EBREAK, MRET and the six Zicsr instructions. +// Anything else sets `illegal`; the EX stage turns that into a trap. +// ============================================================================= +module rabbit5_decoder + import rabbit5_pkg::*; +( + input logic [31:0] instr_i, + output decoded_t dec_o +); + + // Instruction fields (names from the RISC-V spec) + logic [6:0] opcode; + logic [2:0] funct3; + logic [6:0] funct7; + logic [4:0] rd, rs1, rs2; + assign opcode = instr_i[6:0]; + assign rd = instr_i[11:7]; + assign funct3 = instr_i[14:12]; + assign rs1 = instr_i[19:15]; + assign rs2 = instr_i[24:20]; + assign funct7 = instr_i[31:25]; + + // The five immediate formats, already sign-extended + logic [31:0] imm_i, imm_s, imm_b, imm_u, imm_j; + assign imm_i = {{20{instr_i[31]}}, instr_i[31:20]}; + assign imm_s = {{20{instr_i[31]}}, instr_i[31:25], instr_i[11:7]}; + assign imm_b = {{19{instr_i[31]}}, instr_i[31], instr_i[7], instr_i[30:25], instr_i[11:8], 1'b0}; + assign imm_u = {instr_i[31:12], 12'b0}; + assign imm_j = {{11{instr_i[31]}}, instr_i[31], instr_i[19:12], instr_i[20], instr_i[30:21], 1'b0}; + + always_comb begin + // ---- defaults: a harmless no-op that reads and writes nothing ---------- + dec_o = '0; + dec_o.rs1 = rs1; + dec_o.rs2 = rs2; + dec_o.rd = rd; + dec_o.funct3 = funct3; + dec_o.alu_op = ALU_ADD; + dec_o.opa = OPA_RS1; + dec_o.opb = OPB_IMM; + dec_o.res = RES_ALU; + dec_o.imm = imm_i; + + unique case (opcode) + OPC_LUI: begin // rd = imm + dec_o.writes_rd = 1'b1; + dec_o.opa = OPA_ZERO; + dec_o.imm = imm_u; + end + + OPC_AUIPC: begin // rd = pc + imm + dec_o.writes_rd = 1'b1; + dec_o.opa = OPA_PC; + dec_o.imm = imm_u; + end + + OPC_JAL: begin // rd = pc + 4; pc = pc + imm + dec_o.is_jal = 1'b1; + dec_o.writes_rd = 1'b1; + dec_o.res = RES_PC4; + dec_o.imm = imm_j; + end + + OPC_JALR: begin // rd = pc + 4; pc = (rs1 + imm) & ~1 + dec_o.is_jalr = 1'b1; + dec_o.uses_rs1 = 1'b1; + dec_o.writes_rd = 1'b1; + dec_o.res = RES_PC4; + dec_o.illegal = (funct3 != 3'b000); + end + + OPC_BRANCH: begin // if (rs1 ? rs2) pc = pc + imm + dec_o.is_branch = 1'b1; + dec_o.uses_rs1 = 1'b1; + dec_o.uses_rs2 = 1'b1; + dec_o.imm = imm_b; + dec_o.illegal = (funct3 == 3'b010) || (funct3 == 3'b011); + end + + OPC_LOAD: begin // rd = mem[rs1 + imm] + dec_o.is_load = 1'b1; + dec_o.uses_rs1 = 1'b1; + dec_o.writes_rd = 1'b1; + dec_o.illegal = (funct3 == 3'b011) || (funct3 == 3'b110) || (funct3 == 3'b111); + end + + OPC_STORE: begin // mem[rs1 + imm] = rs2 + dec_o.is_store = 1'b1; + dec_o.uses_rs1 = 1'b1; + dec_o.uses_rs2 = 1'b1; + dec_o.imm = imm_s; + dec_o.illegal = (funct3[2] == 1'b1) || (funct3 == 3'b011); + end + + OPC_OP_IMM: begin // rd = rs1 op imm + dec_o.uses_rs1 = 1'b1; + dec_o.writes_rd = 1'b1; + unique case (funct3) + 3'b000: dec_o.alu_op = ALU_ADD; + 3'b010: dec_o.alu_op = ALU_SLT; + 3'b011: dec_o.alu_op = ALU_SLTU; + 3'b100: dec_o.alu_op = ALU_XOR; + 3'b110: dec_o.alu_op = ALU_OR; + 3'b111: dec_o.alu_op = ALU_AND; + 3'b001: begin + dec_o.alu_op = ALU_SLL; + dec_o.illegal = (funct7 != 7'b000_0000); + end + 3'b101: begin + dec_o.alu_op = funct7[5] ? ALU_SRA : ALU_SRL; + dec_o.illegal = (funct7 != 7'b000_0000) && (funct7 != 7'b010_0000); + end + default: ; + endcase + end + + OPC_OP: begin // rd = rs1 op rs2 + dec_o.uses_rs1 = 1'b1; + dec_o.uses_rs2 = 1'b1; + dec_o.writes_rd = 1'b1; + dec_o.opb = OPB_RS2; + unique case (funct3) + 3'b000: dec_o.alu_op = funct7[5] ? ALU_SUB : ALU_ADD; + 3'b001: dec_o.alu_op = ALU_SLL; + 3'b010: dec_o.alu_op = ALU_SLT; + 3'b011: dec_o.alu_op = ALU_SLTU; + 3'b100: dec_o.alu_op = ALU_XOR; + 3'b101: dec_o.alu_op = funct7[5] ? ALU_SRA : ALU_SRL; + 3'b110: dec_o.alu_op = ALU_OR; + 3'b111: dec_o.alu_op = ALU_AND; + default: ; + endcase + // only ADD/SUB and SRL/SRA have a second encoding (funct7 = 0100000) + if (funct7 == 7'b010_0000) + dec_o.illegal = (funct3 != 3'b000) && (funct3 != 3'b101); + else + dec_o.illegal = (funct7 != 7'b000_0000); + end + + OPC_MISC_MEM: begin // FENCE: no caches, no reordering -> no-op + dec_o.illegal = (funct3 != 3'b000); + end + + OPC_SYSTEM: begin + if (funct3 == 3'b000) begin + // ECALL / EBREAK / MRET / WFI: rd and rs1 fields must be zero + unique case (instr_i[31:20]) + 12'h000: dec_o.is_ecall = 1'b1; + 12'h001: dec_o.is_ebreak = 1'b1; + 12'h302: dec_o.is_mret = 1'b1; + 12'h105: ; // WFI: no-op (no interrupts in v0) + default: dec_o.illegal = 1'b1; + endcase + if (rd != 5'd0 || rs1 != 5'd0) dec_o.illegal = 1'b1; + end else if (funct3 == 3'b100) begin + dec_o.illegal = 1'b1; + end else begin + // CSRRW/CSRRS/CSRRC (funct3[2]=0) and CSRRWI/CSRRSI/CSRRCI (funct3[2]=1). + // For the I-forms the rs1 field is a 5-bit zero-extended immediate. + dec_o.is_csr = 1'b1; + dec_o.writes_rd = 1'b1; + dec_o.res = RES_CSR; + dec_o.uses_rs1 = !funct3[2]; + dec_o.imm = {27'b0, rs1}; + end + end + + default: dec_o.illegal = 1'b1; + endcase + + // Compressed (16-bit) encodings are not supported + if (instr_i[1:0] != 2'b11) dec_o.illegal = 1'b1; + + // Writing x0 is "no write" for every later stage + if (rd == 5'd0) dec_o.writes_rd = 1'b0; + + // An illegal instruction reads and writes nothing + if (dec_o.illegal) begin + dec_o.uses_rs1 = 1'b0; + dec_o.uses_rs2 = 1'b0; + dec_o.writes_rd = 1'b0; + dec_o.is_load = 1'b0; + dec_o.is_store = 1'b0; + dec_o.is_branch = 1'b0; + dec_o.is_jal = 1'b0; + dec_o.is_jalr = 1'b0; + dec_o.is_csr = 1'b0; + dec_o.is_ecall = 1'b0; + dec_o.is_ebreak = 1'b0; + dec_o.is_mret = 1'b0; + end + end + +endmodule diff --git a/rtl/cores/rabbit5/rabbit5_pkg.sv b/rtl/cores/rabbit5/rabbit5_pkg.sv new file mode 100644 index 0000000..6533d6d --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_pkg.sv @@ -0,0 +1,109 @@ +// ============================================================================= +// rabbit5_pkg — shared types for the rabbit5 core +// ============================================================================= +// rabbit5 is a classic 5-stage, single-issue, in-order RV32I pipeline: +// +// IF ──► ID ──► EX ──► MEM ──► WB +// +// Design goal: *timing you can reason about*. Every rule that decides how many +// cycles an instruction takes is listed in rabbit5_core.sv ("TIMING RULES") and +// is checked formally in dv/formal/rabbit5/timing/. +// +// Everything that is "a fact about RISC-V" (opcodes, CSR numbers, cause codes) +// lives here, so the pipeline file only contains pipeline logic. +// ============================================================================= +package rabbit5_pkg; + + // --------------------------------------------------------------------------- + // RV32I major opcodes (instruction bits [6:0]) + // --------------------------------------------------------------------------- + localparam logic [6:0] OPC_LOAD = 7'b000_0011; + localparam logic [6:0] OPC_MISC_MEM = 7'b000_1111; // FENCE + localparam logic [6:0] OPC_OP_IMM = 7'b001_0011; + localparam logic [6:0] OPC_AUIPC = 7'b001_0111; + localparam logic [6:0] OPC_STORE = 7'b010_0011; + localparam logic [6:0] OPC_OP = 7'b011_0011; + localparam logic [6:0] OPC_LUI = 7'b011_0111; + localparam logic [6:0] OPC_BRANCH = 7'b110_0011; + localparam logic [6:0] OPC_JALR = 7'b110_0111; + localparam logic [6:0] OPC_JAL = 7'b110_1111; + localparam logic [6:0] OPC_SYSTEM = 7'b111_0011; // ECALL, EBREAK, MRET, WFI, CSR* + + // --------------------------------------------------------------------------- + // ALU operations + // --------------------------------------------------------------------------- + typedef enum logic [3:0] { + ALU_ADD, ALU_SUB, + ALU_SLL, ALU_SRL, ALU_SRA, + ALU_SLT, ALU_SLTU, + ALU_XOR, ALU_OR, ALU_AND + } alu_op_e; + + // Where the ALU's two operands come from + typedef enum logic [1:0] { OPA_RS1, OPA_PC, OPA_ZERO } opa_sel_e; + typedef enum logic { OPB_RS2, OPB_IMM } opb_sel_e; + + // What the EX stage hands on as the instruction's result + typedef enum logic [1:0] { + RES_ALU, // arithmetic, LUI, AUIPC, address for loads/stores + RES_PC4, // JAL / JALR link value + RES_CSR // old CSR value for CSRRW/CSRRS/CSRRC(I) + } res_sel_e; + + // --------------------------------------------------------------------------- + // Decoded instruction: everything later stages need to know, produced once + // by rabbit5_decoder in ID. + // --------------------------------------------------------------------------- + typedef struct packed { + logic illegal; // not a supported instruction -> trap in EX + logic [4:0] rs1; + logic [4:0] rs2; + logic [4:0] rd; + logic uses_rs1; // operand really read (for hazards and RVFI) + logic uses_rs2; + logic writes_rd; // writes a register other than x0 + logic [31:0] imm; // sign-extended immediate (zimm for CSR*I) + alu_op_e alu_op; + opa_sel_e opa; + opb_sel_e opb; + res_sel_e res; + logic [2:0] funct3; // branch condition / memory size / CSR op + logic is_load; + logic is_store; + logic is_branch; + logic is_jal; + logic is_jalr; + logic is_csr; + logic is_ecall; + logic is_ebreak; + logic is_mret; + } decoded_t; + + // --------------------------------------------------------------------------- + // Machine-mode CSRs implemented in v0 (addresses from the privileged spec) + // --------------------------------------------------------------------------- + localparam logic [11:0] CSR_MSTATUS = 12'h300; + localparam logic [11:0] CSR_MISA = 12'h301; + localparam logic [11:0] CSR_MTVEC = 12'h305; + localparam logic [11:0] CSR_MSCRATCH = 12'h340; + localparam logic [11:0] CSR_MEPC = 12'h341; + localparam logic [11:0] CSR_MCAUSE = 12'h342; + localparam logic [11:0] CSR_MTVAL = 12'h343; + localparam logic [11:0] CSR_MCYCLE = 12'hB00; + localparam logic [11:0] CSR_MINSTRET = 12'hB02; + localparam logic [11:0] CSR_MCYCLEH = 12'hB80; + localparam logic [11:0] CSR_MINSTRETH= 12'hB82; + localparam logic [11:0] CSR_MHARTID = 12'hF14; + + // misa: MXL=1 (32-bit), extension I only + localparam logic [31:0] MISA_VALUE = 32'h4000_0100; + + // Exception cause codes (mcause) + localparam logic [31:0] CAUSE_INSN_MISALIGNED = 32'd0; + localparam logic [31:0] CAUSE_ILLEGAL_INSN = 32'd2; + localparam logic [31:0] CAUSE_BREAKPOINT = 32'd3; + localparam logic [31:0] CAUSE_LOAD_MISALIGNED = 32'd4; + localparam logic [31:0] CAUSE_STORE_MISALIGNED = 32'd6; + localparam logic [31:0] CAUSE_ECALL_M = 32'd11; + +endpackage diff --git a/rtl/cores/rabbit5/rabbit5_regfile.sv b/rtl/cores/rabbit5/rabbit5_regfile.sv new file mode 100644 index 0000000..e8bac8c --- /dev/null +++ b/rtl/cores/rabbit5/rabbit5_regfile.sv @@ -0,0 +1,32 @@ +// ============================================================================= +// rabbit5_regfile — 32 x 32-bit registers, 2 read ports, 1 write port +// ============================================================================= +// x0 always reads as zero. +// "Write-first" bypass: if WB writes a register in the same cycle that ID +// reads it, ID sees the *new* value. This removes the WB->ID hazard, so the +// EX-stage forwarding only has to look at MEM and WB. +// ============================================================================= +module rabbit5_regfile ( + input logic clk_i, + input logic [4:0] raddr_a_i, + output logic [31:0] rdata_a_o, + input logic [4:0] raddr_b_i, + output logic [31:0] rdata_b_o, + input logic we_i, + input logic [4:0] waddr_i, + input logic [31:0] wdata_i +); + logic [31:0] regs [32]; + + always_ff @(posedge clk_i) + if (we_i && waddr_i != 5'd0) regs[waddr_i] <= wdata_i; + + function automatic logic [31:0] read(input logic [4:0] addr); + if (addr == 5'd0) return 32'b0; + else if (we_i && waddr_i == addr) return wdata_i; // bypass + else return regs[addr]; + endfunction + + assign rdata_a_o = read(raddr_a_i); + assign rdata_b_o = read(raddr_b_i); +endmodule diff --git a/rtl/cores/rabbit5/rabbit_cpu.sv b/rtl/cores/rabbit5/rabbit_cpu.sv new file mode 100644 index 0000000..1813c08 --- /dev/null +++ b/rtl/cores/rabbit5/rabbit_cpu.sv @@ -0,0 +1,54 @@ +// rabbit_cpu adapter for rabbit5 (our own 5-stage RV32I core). +// See rtl/cores/README.md for the port contract. rabbit5 needs memories that +// grant immediately and answer one cycle later (rabbit5_core.sv, rule R4). +module rabbit_cpu #( + parameter logic [31:0] BOOT_ADDR = 32'h0000_0080, + parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000 +) ( + input logic clk_i, + input logic rst_ni, + input logic fetch_enable_i, + + output logic instr_req_o, + input logic instr_gnt_i, + input logic instr_rvalid_i, + output logic [31:0] instr_addr_o, + input logic [31:0] instr_rdata_i, + + output logic data_req_o, + input logic data_gnt_i, + input logic data_rvalid_i, + output logic data_we_o, + output logic [ 3:0] data_be_o, + output logic [31:0] data_addr_o, + output logic [31:0] data_wdata_o, + input logic [31:0] data_rdata_i, + + input logic [31:0] irq_i, + output logic irq_ack_o, + output logic [ 4:0] irq_id_o, + + input logic debug_req_i, + output logic core_sleep_o +); + rabbit5_core #(.BOOT_ADDR(BOOT_ADDR), .MTVEC_ADDR(MTVEC_ADDR)) u_core ( + .clk_i, .rst_ni, .fetch_enable_i, + .instr_req_o, .instr_gnt_i, .instr_rvalid_i, .instr_addr_o, .instr_rdata_i, + .data_req_o, .data_gnt_i, .data_rvalid_i, .data_we_o, .data_be_o, + .data_addr_o, .data_wdata_o, .data_rdata_i, + .irq_i, + // RVFI is only used by formal and trace tools + .rvfi_valid(), .rvfi_order(), .rvfi_insn(), .rvfi_trap(), .rvfi_halt(), + .rvfi_intr(), .rvfi_mode(), .rvfi_ixl(), .rvfi_rs1_addr(), .rvfi_rs2_addr(), + .rvfi_rs1_rdata(), .rvfi_rs2_rdata(), .rvfi_rd_addr(), .rvfi_rd_wdata(), + .rvfi_pc_rdata(), .rvfi_pc_wdata(), .rvfi_mem_addr(), .rvfi_mem_rmask(), + .rvfi_mem_wmask(), .rvfi_mem_rdata(), .rvfi_mem_wdata() + ); + + // v0 has no interrupts and no debug module + assign irq_ack_o = 1'b0; + assign irq_id_o = 5'd0; + assign core_sleep_o = 1'b0; + logic unused; + assign unused = debug_req_i; +endmodule diff --git a/rtl/soc/rabbit_soc_sim.sv b/rtl/soc/rabbit_soc_sim.sv index c889ae4..2d6aa50 100644 --- a/rtl/soc/rabbit_soc_sim.sv +++ b/rtl/soc/rabbit_soc_sim.sv @@ -27,10 +27,17 @@ module rabbit_soc_sim #( logic [ 3:0] data_be; logic [31:0] data_addr, data_wdata, data_rdata; + // A gate-level netlist has its parameters baked in at synthesis time + // (the rabbit_cpu defaults: BOOT_ADDR = 0x80, MTVEC_ADDR = 0x0), so it + // cannot be re-parameterised here. +`ifdef RABBIT_GLS + rabbit_cpu u_cpu ( +`else rabbit_cpu #( .BOOT_ADDR (32'h0000_0080), .MTVEC_ADDR(32'h0000_0000) ) u_cpu ( +`endif .clk_i, .rst_ni, .fetch_enable_i(1'b1), .instr_req_o(instr_req), .instr_gnt_i(instr_gnt), .instr_rvalid_i(instr_rvalid), diff --git a/sw/baremetal/Makefile b/sw/baremetal/Makefile index 8f90727..a0bc395 100644 --- a/sw/baremetal/Makefile +++ b/sw/baremetal/Makefile @@ -1,5 +1,5 @@ # Build a bare-metal program for the selected core. -# make PROG=hello -> build/hello/hello.{elf,hex,dis} +# make PROG=hello -> build/$(CORE)/hello/hello.{elf,hex,dis} # make PROG=hello CORE=ibex (once an ibex adapter exists) REPO ?= $(abspath ../..) CORE ?= cv32e40p @@ -13,7 +13,7 @@ OBJCOPY= $(CROSS)objcopy OBJDUMP= $(CROSS)objdump COMMON = $(REPO)/sw/baremetal/common -OUT = build/$(PROG) +OUT = build/$(CORE)/$(PROG) CFLAGS = -march=$(CORE_MARCH) -mabi=$(CORE_MABI) -O2 -g -Wall -Wextra \ -ffreestanding -fno-builtin -nostdlib -I$(COMMON) diff --git a/third_party/riscv-formal b/third_party/riscv-formal new file mode 160000 index 0000000..c992aa6 --- /dev/null +++ b/third_party/riscv-formal @@ -0,0 +1 @@ +Subproject commit c992aa61fdfe0846c5ed90324c596202a1c69b76 diff --git a/tools/gls/README.md b/tools/gls/README.md index 9f54596..1357f0b 100644 --- a/tools/gls/README.md +++ b/tools/gls/README.md @@ -12,7 +12,6 @@ rabbit SoC fast enough to run a real regression, not just one smoke test. X-propagation, SKY130 / GF180 / IHP support, CUDA/HIP/Metal). - **No published accuracy/speed comparison on a real post-layout RISC-V netlist was found.** That benchmark alone is publishable. - (Details and sources: `docs/research/2026-11-04-soc-5yr-plan.md`, A.7–A.8.) ## Staged plan