From 413ac2276b9d431a53ee095de31ea47d73c832de Mon Sep 17 00:00:00 2001 From: abmajith Date: Fri, 6 Nov 2026 12:20:01 +0100 Subject: [PATCH] rabbit_common + rabbit3: shared core library and a 3-stage RV32I core - rtl/cores/rabbit_common: decoder, ALU, regfile, CSRs moved out of rabbit5; new rabbit_execute (whole execute stage: operands, branches, exceptions, CSRs, next pc -> exec_t record) and rabbit_rvfi; LSU/branch helpers in rabbit_pkg - rabbit5_core.sv now only the pipeline (496 -> 278 lines); same 3958 cycles for hello, riscv-formal 45/45 - rabbit3: F | X | W pipeline from the same blocks; no forwarding network and no load-use stall (regfile write-first bypass), 1-bubble redirects; hello 3145 cycles, riscv-formal 45/45, timing properties, GLS smoke - dv/formal/rabbit: one flow for every core (CORE=rabbit3|rabbit5); each core declares its timing model in core.mk and the shared timing testbench proves it - fix: timing testbench free inputs are now top-level inputs; slang silently drops (* anyseq *), which made the earlier rabbit5 timing proof weaker than reported. Re-proven and re-mutation-tested. - riscv-formal cover moved to step 10 (exact counts at step 20 took up to 14 min; the bounds are proven in the timing testbench instead) - CI: rabbit3 in all matrices; formal and GLS per core - docs: rabbit3 "start here" learning path, rabbit_common overview Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 41 ++- .gitignore | 6 +- Makefile | 8 +- docs/STATUS.md | 15 +- dv/formal/README.md | 60 +++- dv/formal/rabbit/Makefile | 77 ++++ dv/formal/rabbit/checks.cfg | 38 ++ dv/formal/{rabbit5 => rabbit}/summary.py | 0 .../timing/rabbit_timing_tb.sv} | 66 ++-- dv/formal/rabbit/timing/timing.sby.in | 20 ++ dv/formal/{rabbit5 => rabbit}/wrapper.sv | 6 +- dv/formal/rabbit5/Makefile | 64 ---- dv/formal/rabbit5/checks.cfg | 35 -- dv/formal/rabbit5/timing/timing.sby | 29 -- rtl/cores/README.md | 4 +- rtl/cores/rabbit3/README.md | 68 ++++ rtl/cores/rabbit3/core.mk | 11 + rtl/cores/rabbit3/files.f | 11 + rtl/cores/rabbit3/rabbit3_core.sv | 201 +++++++++++ rtl/cores/rabbit3/rabbit_cpu.sv | 54 +++ rtl/cores/rabbit5/README.md | 34 +- rtl/cores/rabbit5/core.mk | 6 + rtl/cores/rabbit5/files.f | 15 +- rtl/cores/rabbit5/rabbit5_core.sv | 329 +++--------------- rtl/cores/rabbit_common/README.md | 37 ++ .../rabbit_alu.sv} | 6 +- .../rabbit_csr.sv} | 6 +- .../rabbit_decoder.sv} | 6 +- rtl/cores/rabbit_common/rabbit_execute.sv | 149 ++++++++ .../rabbit_pkg.sv} | 104 +++++- .../rabbit_regfile.sv} | 4 +- rtl/cores/rabbit_common/rabbit_rvfi.sv | 72 ++++ 32 files changed, 1065 insertions(+), 517 deletions(-) create mode 100644 dv/formal/rabbit/Makefile create mode 100644 dv/formal/rabbit/checks.cfg rename dv/formal/{rabbit5 => rabbit}/summary.py (100%) rename dv/formal/{rabbit5/timing/rabbit5_timing_tb.sv => rabbit/timing/rabbit_timing_tb.sv} (71%) create mode 100644 dv/formal/rabbit/timing/timing.sby.in rename dv/formal/{rabbit5 => rabbit}/wrapper.sv (87%) delete mode 100644 dv/formal/rabbit5/Makefile delete mode 100644 dv/formal/rabbit5/checks.cfg delete mode 100644 dv/formal/rabbit5/timing/timing.sby create mode 100644 rtl/cores/rabbit3/README.md create mode 100644 rtl/cores/rabbit3/core.mk create mode 100644 rtl/cores/rabbit3/files.f create mode 100644 rtl/cores/rabbit3/rabbit3_core.sv create mode 100644 rtl/cores/rabbit3/rabbit_cpu.sv create mode 100644 rtl/cores/rabbit_common/README.md rename rtl/cores/{rabbit5/rabbit5_alu.sv => rabbit_common/rabbit_alu.sv} (88%) rename rtl/cores/{rabbit5/rabbit5_csr.sv => rabbit_common/rabbit_csr.sv} (97%) rename rtl/cores/{rabbit5/rabbit5_decoder.sv => rabbit_common/rabbit_decoder.sv} (98%) create mode 100644 rtl/cores/rabbit_common/rabbit_execute.sv rename rtl/cores/{rabbit5/rabbit5_pkg.sv => rabbit_common/rabbit_pkg.sv} (51%) rename rtl/cores/{rabbit5/rabbit5_regfile.sv => rabbit_common/rabbit_regfile.sv} (92%) create mode 100644 rtl/cores/rabbit_common/rabbit_rvfi.sv diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 659a019..5a81579 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -21,7 +21,7 @@ jobs: strategy: fail-fast: false matrix: - core: [cv32e40p, rabbit5] + core: [cv32e40p, rabbit3, rabbit5] steps: - uses: actions/checkout@v4 with: { submodules: recursive } @@ -34,7 +34,7 @@ jobs: strategy: fail-fast: false matrix: - core: [cv32e40p, rabbit5] + core: [cv32e40p, rabbit3, rabbit5] prog: [hello] steps: - name: RISC-V GCC @@ -68,51 +68,66 @@ 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. + # riscv-formal (45 checks) + timing properties, for each of our own cores. formal: runs-on: ubuntu-24.04 + strategy: + fail-fast: false + matrix: + core: [rabbit3, rabbit5] 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 + - run: make formal CORE=${{ matrix.core }} - uses: actions/upload-artifact@v4 if: failure() with: - name: formal-results + name: formal-results-${{ matrix.core }} 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 + dv/formal/rabbit/build/${{ matrix.core }}/riscv-formal/cores/${{ matrix.core }}/checks/*/logfile.txt + dv/formal/rabbit/build/${{ matrix.core }}/riscv-formal/cores/${{ matrix.core }}/checks/*/engine_0/*.vcd + dv/formal/rabbit/build/${{ matrix.core }}/timing_*/logfile.txt + dv/formal/rabbit/build/${{ matrix.core }}/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 + strategy: + matrix: + core: [rabbit3, rabbit5] steps: - uses: actions/checkout@v4 - uses: YosysHQ/setup-oss-cad-suite@v3 with: { version: "2026-11-04" } - - run: make gls-netlist CORE=rabbit5 + - run: make gls-netlist CORE=${{ matrix.core }} - uses: actions/upload-artifact@v4 - with: { name: gls-netlist-rabbit5, path: build/gls/rabbit5 } + with: + name: gls-netlist-${{ matrix.core }} + path: build/gls/${{ matrix.core }} gls-smoke: needs: gls-netlist runs-on: ubuntu-24.04 container: { image: "verilator/verilator:v5.054", options: --entrypoint "" } + strategy: + fail-fast: false + matrix: + core: [rabbit3, rabbit5] 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 } + with: + name: gls-netlist-${{ matrix.core }} + path: build/gls/${{ matrix.core }} - run: uv sync - working-directory: dv/cocotb/soc - run: uv run make CORE=rabbit5 PROG=hello GLS=1 + run: uv run make CORE=${{ matrix.core }} PROG=hello GLS=1 rma-smoke: runs-on: ubuntu-24.04 diff --git a/.gitignore b/.gitignore index 5f22c8c..d97f3a3 100644 --- a/.gitignore +++ b/.gitignore @@ -36,6 +36,6 @@ sw/baremetal/build/ **/sim_build_*/ **/*.fst build/ -dv/formal/rabbit5/build/ -dv/formal/rabbit5/timing/timing_*/ -dv/formal/rabbit5/timing/timing/ +dv/formal/rabbit/build/ +dv/formal/rabbit/*.log +dv/formal/rabbit/timing/timing*/ diff --git a/Makefile b/Makefile index 880e7cf..f995e01 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ # 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 formal riscv-formal + timing properties (CORE=rabbit3|rabbit5) # make gls-smoke synthesize the core with Yosys, run firmware on the netlist # make ci everything CI runs REPO := $(abspath .) @@ -61,8 +61,10 @@ rma-smoke: sync done # ---- formal (rabbit5) --------------------------------------------------------- +# formal works on our own cores; with the default CORE (cv32e40p) it runs rabbit5 +FORMAL_CORE := $(if $(filter rabbit%,$(CORE)),$(CORE),rabbit5) formal: - $(MAKE) -C dv/formal/rabbit5 + $(MAKE) -C dv/formal/rabbit CORE=$(FORMAL_CORE) # ---- gate-level smoke test: generic Yosys gates, zero delay ---------------------- # Catches RTL that simulates differently from what synthesizes (latches, X, @@ -87,7 +89,7 @@ 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_* + rm -rf build dv/formal/rabbit/build cd hw_ip/sim && uv run $(MAKE) clean .PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke formal gls-netlist gls-smoke ci clean diff --git a/docs/STATUS.md b/docs/STATUS.md index acb7df5..e9145ca 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -10,18 +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` +## Own cores: rabbit3 and rabbit5 (shared blocks in rtl/cores/rabbit_common) -| Item | Command | Result | +| Item | rabbit3 (3-stage) | rabbit5 (5-stage) | |---|---|---| -| 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 | +| hello (`make soc-sim CORE=...`) | PASS, 3145 cycles | PASS, 3958 cycles | +| riscv-formal (`make formal CORE=...`) | 45/45 | 45/45 | +| timing properties T1–T3 + covers | PASS | PASS | +| gate-level smoke (`make gls-smoke CORE=...`) | PASS, same cycles | PASS, same cycles | +| size, Yosys generic gates | 10.3 k cells | 11.1 k cells | 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`. +Learning path: `rtl/cores/rabbit3/README.md`. ## Known issues diff --git a/dv/formal/README.md b/dv/formal/README.md index 706952c..f61e850 100644 --- a/dv/formal/README.md +++ b/dv/formal/README.md @@ -1,26 +1,42 @@ # dv/formal — formal verification -## rabbit5 (working) +## rabbit cores (rabbit3, rabbit5) + +One flow for every rabbit core, selected with `CORE=`: ```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 +make formal CORE=rabbit3 # from the repo root: everything below +make -C dv/formal/rabbit CORE=rabbit5 riscv-formal +make -C dv/formal/rabbit CORE=rabbit5 timing +make -C dv/formal/rabbit CORE=rabbit3 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/` | +| **riscv-formal** (YosysHQ, submodule) | every RV32I instruction computes what the ISA says (37 checks), plus pipeline consistency: `reg` (forwarding/bypass), `pc_fwd`/`pc_bwd` (branches, flushes), `causal`, `unique`, `liveness`, `ill`, `cover` | `rabbit/checks.cfg` (template), `rabbit/wrapper.sv` | +| **timing properties** (ours) | T1 exact retirement-gap model, T2 first retirement cycle, T3 memory used exactly one cycle before retirement; covers prove every case and the min/max throughput bounds are reachable | `rabbit/timing/rabbit_timing_tb.sv` | + +Each core **declares** its timing model in `rtl/cores//core.mk` +(`TIMING_FIRST_RETIRE`, `TIMING_REDIRECT_GAP`, `TIMING_LOADUSE_GAP`); the same +timing testbench then proves the core matches its declaration. + +| | rabbit3 | rabbit5 | +|---|---|---| +| riscv-formal | 45/45 PASS | 45/45 PASS | +| timing T1–T3 + covers | PASS | PASS | +| wall time, 22 cores | ~4 min (`reg`, `pc_fwd`, `pc_bwd` dominate) | ~30 s | + +rabbit3 is *harder* to prove: its single X stage contains memory → bypass → +execute → data address as one cycle of logic, and the cross-instruction checks +(`reg`, `pc_fwd`, `pc_bwd`) must reason through all of it at every step. 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`). +1. The cores are 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//core_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. + 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). @@ -28,9 +44,23 @@ 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. +### Mutation results (the checks are not vacuous) + +| Planted bug | Caught by | +|---|---| +| rabbit5: forwarding priority MEM/WB swapped | only riscv-formal `reg_ch0` | +| rabbit5: stall on every EX dependency (not only loads) | timing T1 (riscv-formal passes) | +| rabbit3 checked against REDIRECT_GAP=3 / LOADUSE_GAP=2 | timing T1 + covers | +| rabbit5 checked against LOADUSE_GAP=1 | timing T1 + covers | + +### Lesson learned: free inputs must be real inputs + +`(* anyseq *)` on an internal signal is **silently ignored by the slang +frontend**; the signal becomes a constant `x`, which the solver may choose +differently at every place it is used — the decoder can then "see" a different +instruction than the pipeline register stores. The timing testbench therefore +takes the instruction word and load data as **top-level inputs**. The first +rabbit5 timing result (before 2026-11-06) had this flaw and was re-proven. ## Planned diff --git a/dv/formal/rabbit/Makefile b/dv/formal/rabbit/Makefile new file mode 100644 index 0000000..b7ec2b1 --- /dev/null +++ b/dv/formal/rabbit/Makefile @@ -0,0 +1,77 @@ +# Formal verification of a rabbit core: make CORE=rabbit3 (default rabbit5) +# make riscv-formal checks + timing properties +# make riscv-formal only riscv-formal (parallel) +# make timing only the timing properties (timing/rabbit_timing_tb.sv) +# make check C=insn_add_ch0 one riscv-formal check +REPO ?= $(abspath ../../..) +CORE ?= rabbit5 +JOBS ?= $(shell nproc) +RF_SRC := $(REPO)/third_party/riscv-formal + +include $(REPO)/rtl/cores/$(CORE)/core.mk + +# all SystemVerilog sources of the core except the rabbit_cpu adapter +SOURCES := $(shell grep -v '^//' $(REPO)/rtl/cores/$(CORE)/files.f | grep -v rabbit_cpu.sv | sed 's|$${REPO}|$(REPO)|') + +BUILD := build/$(CORE) +FLAT := $(BUILD)/core_flat.v +# genchecks.py expects /cores//, so build a small mirror +MIRROR := $(BUILD)/riscv-formal +CORE_DIR := $(MIRROR)/cores/$(CORE) + +# 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) + +all: riscv-formal timing + +# ---- riscv-formal -------------------------------------------------------------- +riscv-formal: generate + $(MAKE) -C $(CORE_DIR)/checks -j$(JOBS) -k + @python3 summary.py $(CORE_DIR)/checks + +generate: $(CORE_DIR)/checks/makefile + +# The cores are 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 $(CORE)_core -DSYNTHESIS; \ + hierarchy -top $(CORE)_core; proc; flatten; opt_clean; \ + write_verilog -noattr $@" + +$(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv + @mkdir -p $(MIRROR) $(CORE_DIR) + ln -sfn $(RF_SRC)/checks $(MIRROR)/checks + ln -sfn $(RF_SRC)/insns $(MIRROR)/insns + cp $(FLAT) wrapper.sv $(CORE_DIR)/ + sed -e 's/@RABBIT_CORE@/$(CORE)_core/' checks.cfg > $(CORE_DIR)/checks.cfg + rm -rf $(CORE_DIR)/checks + cd $(CORE_DIR) && python3 ../../checks/genchecks.py + +check: generate + $(MAKE) -C $(CORE_DIR)/checks $(C) + @cat $(CORE_DIR)/checks/$(C)/status + +# ---- timing properties ------------------------------------------------------------ +# Reads the SystemVerilog through slang directly (much faster to solve than +# the converted file). The core's timing model comes from its core.mk. +TIMING_DEFINES := -DSYNTHESIS -DRABBIT_CORE=$(CORE)_core \ + -DFIRST_RETIRE=$(TIMING_FIRST_RETIRE) \ + -DREDIRECT_GAP=$(TIMING_REDIRECT_GAP) \ + -DLOADUSE_GAP=$(TIMING_LOADUSE_GAP) + +timing: $(BUILD)/timing.sby + cd $(BUILD) && sby -f timing.sby + +$(BUILD)/timing.sby: timing/timing.sby.in timing/rabbit_timing_tb.sv $(SOURCES) + @mkdir -p $(BUILD) + @if [ -n "$(YOSYS_SLANG)" ]; then echo "plugin -i slang" > $(BUILD)/slang_load.ys; \ + else echo "# slang is built in" > $(BUILD)/slang_load.ys; fi + sed -e 's|@SOURCES@|$(notdir $(SOURCES)) rabbit_timing_tb.sv|' \ + -e 's|@DEFINES@|$(TIMING_DEFINES)|' timing/timing.sby.in > $@ + printf '%s\n' $(SOURCES) $(abspath timing/rabbit_timing_tb.sv) $(abspath $(BUILD))/slang_load.ys >> $@ + +clean: + rm -rf build + +.PHONY: all riscv-formal generate check timing clean diff --git a/dv/formal/rabbit/checks.cfg b/dv/formal/rabbit/checks.cfg new file mode 100644 index 0000000..8bfaebd --- /dev/null +++ b/dv/formal/rabbit/checks.cfg @@ -0,0 +1,38 @@ +# riscv-formal configuration TEMPLATE for the rabbit cores (see dv/formal/README.md). +# The Makefile fills in @RABBIT_CORE@ for CORE=rabbit3|rabbit5. +# +# [depth] columns: [start] [step to check at] (BMC cycles) +# The first instruction retires 3 (rabbit3) or 5 (rabbit5) cycles after reset. + +[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 8 15 +ill 12 +cover 1 10 + +[sort] +reg_ch0 + +[defines] +`define RISCV_FORMAL_ALIGNED_MEM +`define RABBIT_CORE @RABBIT_CORE@ + +[verilog-files] +@basedir@/cores/@core@/wrapper.sv +@basedir@/cores/@core@/core_flat.v + +[cover] +# Non-vacuity only: instructions really retire within the check depth, and a +# trap is reachable. The exact timing model and the min/max throughput bounds +# are proven in timing/rabbit_timing_tb.sv, where the solver needs seconds +# (asking riscv-formal's bigger testbench for exact counts took up to 14 min). +always @* if (!reset) cover (channel[0].cnt_insns >= 4); +always @* if (!reset) cover (channel[0].valid && channel[0].trap); diff --git a/dv/formal/rabbit5/summary.py b/dv/formal/rabbit/summary.py similarity index 100% rename from dv/formal/rabbit5/summary.py rename to dv/formal/rabbit/summary.py diff --git a/dv/formal/rabbit5/timing/rabbit5_timing_tb.sv b/dv/formal/rabbit/timing/rabbit_timing_tb.sv similarity index 71% rename from dv/formal/rabbit5/timing/rabbit5_timing_tb.sv rename to dv/formal/rabbit/timing/rabbit_timing_tb.sv index 3c638b6..b823640 100644 --- a/dv/formal/rabbit5/timing/rabbit5_timing_tb.sv +++ b/dv/formal/rabbit/timing/rabbit_timing_tb.sv @@ -1,17 +1,24 @@ // ============================================================================= -// rabbit5 timing properties (beyond riscv-formal) +// rabbit timing properties (beyond riscv-formal) — one testbench, every core // ============================================================================= // riscv-formal proves WHAT each instruction computes. These properties prove -// WHEN: they turn the "TIMING RULES" comment in rabbit5_core.sv into checked +// WHEN: they turn the "TIMING RULES" comment of a rabbit core 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. +// core as a black box. +// +// The core and its timing model come from rtl/cores//core.mk, passed in +// as macros by the Makefile: +// RABBIT_CORE module name (rabbit3_core / rabbit5_core) +// FIRST_RETIRE cycle of the first retirement after reset (5 / 3) +// REDIRECT_GAP cycles between a redirecting instruction and the next (3 / 2) +// LOADUSE_GAP cycles between a load and an instruction using it (2 / 1) // // 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] +// REDIRECT_GAP if the earlier instruction changed control flow +// (taken branch, JAL, JALR, MRET, trap) [rule R3] +// LOADUSE_GAP if the later one reads the register the +// earlier one loaded (load-use) [rule R2] +// 1 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] @@ -22,14 +29,19 @@ // - 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 +module rabbit_timing_tb ( + input logic clk, + // Free inputs: the solver may choose ANY instruction word and ANY load + // data in every cycle. They are top-level inputs on purpose: an + // (* anyseq *) attribute is silently dropped by the slang frontend, and + // the signal would become a "don't care" constant that the solver may + // choose differently at every place it is used. + input logic [31:0] instr_rdata, + input logic [31:0] data_rdata ); - 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; + localparam int FIRST_RETIRE = `FIRST_RETIRE; + localparam int REDIRECT_GAP = `REDIRECT_GAP; + localparam int LOADUSE_GAP = `LOADUSE_GAP; // ---- reset for exactly the first cycle ------------------------------------- logic rst_n = 1'b0; @@ -41,7 +53,7 @@ module rabbit5_timing_tb ( logic [4:0] rvfi_rs1_addr, rvfi_rs2_addr, rvfi_rd_addr; logic [3:0] rvfi_mem_rmask, rvfi_mem_wmask; - rabbit5_core dut ( + `RABBIT_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), @@ -60,7 +72,7 @@ module rabbit5_timing_tb ( ); // ---- classify the instruction that retires now ------------------------------ - // (the ISA-level meaning only; nothing about how rabbit5 is built) + // (the ISA-level meaning only; nothing about how the core is built) logic [6:0] opcode; logic [2:0] funct3; assign opcode = rvfi_insn[6:0]; @@ -119,7 +131,7 @@ module rabbit5_timing_tb ( (rvfi_rs1_addr == prev_rd || rvfi_rs2_addr == prev_rd); int expected_gap; - assign expected_gap = prev_flow ? 3 : (load_use ? 2 : 1); + assign expected_gap = prev_flow ? REDIRECT_GAP : (load_use ? LOADUSE_GAP : 1); // ---- T1, T2 ------------------------------------------------------------------------ always_comb begin @@ -139,9 +151,12 @@ module rabbit5_timing_tb ( 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. + // From T1 + T2: after the first retirement (cycle FIRST_RETIRE-1), one more + // instruction retires every 1..REDIRECT_GAP cycles. So at cycle 19 between + // MIN_AT_19 and MAX_AT_19 have retired (rabbit5: 6..16, rabbit3: 9..18). // Both extremes must be reachable (covers below). + localparam int MAX_AT_19 = 19 - (FIRST_RETIRE - 1) + 1; + localparam int MIN_AT_19 = (19 - (FIRST_RETIRE - 1)) / REDIRECT_GAP + 1; int retired; always_ff @(posedge clk) begin if (!rst_n) retired <= 0; @@ -153,15 +168,14 @@ module rabbit5_timing_tb ( // ---- 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 + cover (retired_now == MIN_AT_19); // slowest possible: every instruction redirects + cover (retired_now == MAX_AT_19); // 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); + cover (gap == LOADUSE_GAP && load_use); + cover (gap == REDIRECT_GAP); + cover (gap == REDIRECT_GAP && rvfi_trap); end end endmodule diff --git a/dv/formal/rabbit/timing/timing.sby.in b/dv/formal/rabbit/timing/timing.sby.in new file mode 100644 index 0000000..d1691fb --- /dev/null +++ b/dv/formal/rabbit/timing/timing.sby.in @@ -0,0 +1,20 @@ +# Template: the Makefile fills in the core's sources and timing model. +# make -C dv/formal/rabbit timing CORE=rabbit3 +[tasks] +bmc +cover + +[options] +bmc: mode bmc +cover: mode cover +depth 24 + +[engines] +smtbmc boolector + +[script] +script slang_load.ys +read_slang @SOURCES@ --top rabbit_timing_tb @DEFINES@ +prep -top rabbit_timing_tb + +[files] diff --git a/dv/formal/rabbit5/wrapper.sv b/dv/formal/rabbit/wrapper.sv similarity index 87% rename from dv/formal/rabbit5/wrapper.sv rename to dv/formal/rabbit/wrapper.sv index 0b58cb8..f351427 100644 --- a/dv/formal/rabbit5/wrapper.sv +++ b/dv/formal/rabbit/wrapper.sv @@ -1,11 +1,11 @@ -// riscv-formal wrapper for rabbit5. +// riscv-formal wrapper for the rabbit cores (RABBIT_CORE is set by the Makefile). // // 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 +// Memory contract (rule R4 of every rabbit core): requests are granted immediately and the // answer comes one cycle later. We model exactly that and nothing more. module rvfi_wrapper ( input clock, @@ -23,7 +23,7 @@ module rvfi_wrapper ( (* keep *) wire [31:0] data_addr; (* keep *) wire [31:0] data_wdata; - rabbit5_core uut ( + `RABBIT_CORE uut ( .clk_i (clock), .rst_ni (!reset), .fetch_enable_i (1'b1), diff --git a/dv/formal/rabbit5/Makefile b/dv/formal/rabbit5/Makefile deleted file mode 100644 index e9f662d..0000000 --- a/dv/formal/rabbit5/Makefile +++ /dev/null @@ -1,64 +0,0 @@ -# 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 deleted file mode 100644 index 37effc0..0000000 --- a/dv/formal/rabbit5/checks.cfg +++ /dev/null @@ -1,35 +0,0 @@ -# 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/timing/timing.sby b/dv/formal/rabbit5/timing/timing.sby deleted file mode 100644 index 4db2862..0000000 --- a/dv/formal/rabbit5/timing/timing.sby +++ /dev/null @@ -1,29 +0,0 @@ -# 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/rtl/cores/README.md b/rtl/cores/README.md index bd36c7b..9f72405 100644 --- a/rtl/cores/README.md +++ b/rtl/cores/README.md @@ -49,7 +49,9 @@ 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 RV32I core | **working (v0)** | riscv-formal 45/45, timing properties, GLS smoke — see its README | +| `rabbit3/` | Our own 3-stage RV32I core (F/X/W) — **start here** | **working** | riscv-formal 45/45, timing properties, GLS smoke | +| `rabbit5/` | Our own 5-stage, timing-predictable RV32I core | **working** | riscv-formal 45/45, timing properties, GLS smoke | +| `rabbit_common/` | Blocks shared by rabbit3 and rabbit5 (decoder, ALU, regfile, CSRs, execute, RVFI) | — | not a core; listed in each core's `files.f` | 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. diff --git a/rtl/cores/rabbit3/README.md b/rtl/cores/rabbit3/README.md new file mode 100644 index 0000000..43c1aca --- /dev/null +++ b/rtl/cores/rabbit3/README.md @@ -0,0 +1,68 @@ +# rabbit3 — 3-stage RV32I core (start here) + +The smallest rabbit pipeline: **F | X | W**. It is built from exactly the same +blocks as rabbit5 (`../rabbit_common/`); only the pipeline file differs. +Read this core first, then rabbit5, and compare. + +``` +F ──► X ──────────────────────────────────► W + decode, register read, execute, load data arrives, + data request (commit point) register write, RVFI +``` + +## Learning path + +| Step | Read | Ask yourself | +|---|---|---| +| 1 | `../rabbit_common/README.md` | which blocks exist and what each one does | +| 2 | `../rabbit_common/rabbit_pkg.sv` | what is in `decoded_t` and `exec_t`? | +| 3 | `rabbit3_core.sv` (≈200 lines) | how does one instruction move F → X → W? | +| 4 | `../rabbit_common/rabbit_regfile.sv` | why does the write-first bypass make forwarding unnecessary here? | +| 5 | `../rabbit_common/rabbit_execute.sv` | where are branches decided, where do traps come from? | +| 6 | `../rabbit5/rabbit5_core.sv` | what had to be *added* for two more stages: hold register, load-use stall, forwarding | + +Then run both and look at the difference: + +```bash +make soc-sim CORE=rabbit3 # hello: 3145 cycles +make soc-sim CORE=rabbit5 # hello: 3958 cycles +make soc-waves CORE=rabbit3 # waveform: dv/cocotb/soc/dump.fst +make formal CORE=rabbit3 # riscv-formal 45/45 + timing properties +make gls-smoke CORE=rabbit3 # same firmware on the gate netlist +``` + +## Timing rules (`rabbit3_core.sv`), proven by `dv/formal/rabbit/timing` + +| | rabbit3 | rabbit5 | +|---|---|---| +| First instruction retires | cycle 3 | cycle 5 | +| Normal | 1 per cycle | 1 per cycle | +| Load followed by a user of the loaded register | **no penalty** | 1 bubble | +| Taken branch / jump / MRET / trap | **1 bubble** | 2 bubbles | +| Gap between two retirements | 1 or 2 | 1, 2 or 3 | +| `hello` (RV32I, software mul/div) | 3145 cycles | 3958 cycles | +| Size (Yosys generic gates, incl. adapter) | 10.3 k cells | 11.1 k cells | +| Longest combinational path (qualitative) | memory → load align → register bypass → ALU → data address | one stage of that | + +So rabbit3 needs fewer cycles, but each cycle must be longer. Which one is +faster in *time* is decided by the clock frequency each reaches on a real PDK +(sky130 / IHP) — a good first experiment with OpenROAD later. + +## What is shared, what is not + +| | Shared (`rabbit_common`) | rabbit3 only | +|---|---|---| +| Decode, ALU, branch decision, CSRs, traps, next pc | ✔ `rabbit_execute`, `rabbit_decoder` | | +| Register file | ✔ `rabbit_regfile` | | +| RVFI reporting | ✔ `rabbit_rvfi` | | +| Load/store byte lanes and sign extension | ✔ functions in `rabbit_pkg` | | +| Fetch, when the PC moves, what is a bubble | | ✔ `rabbit3_core.sv` | +| Where the data request leaves (X) and the load data returns (W) | | ✔ | + +## Things to try (exercises) + +- Change one line so that a redirect is decided one stage later and watch the + timing proof fail. Then update `core.mk` (`TIMING_REDIRECT_GAP`) and watch + it pass again — the declared timing model is the spec. +- Remove the bypass in `rabbit_regfile.sv` (always return `regs[addr]`): which + riscv-formal check fails, and why for rabbit3 *and* rabbit5? diff --git a/rtl/cores/rabbit3/core.mk b/rtl/cores/rabbit3/core.mk new file mode 100644 index 0000000..d83dda1 --- /dev/null +++ b/rtl/cores/rabbit3/core.mk @@ -0,0 +1,11 @@ +# 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 := + +# Timing model of this core (rabbit3_core.sv, TIMING RULES). The formal +# timing properties in dv/formal/rabbit/timing check the core against these. +TIMING_FIRST_RETIRE := 3 +TIMING_REDIRECT_GAP := 2 +TIMING_LOADUSE_GAP := 1 diff --git a/rtl/cores/rabbit3/files.f b/rtl/cores/rabbit3/files.f new file mode 100644 index 0000000..97bcaef --- /dev/null +++ b/rtl/cores/rabbit3/files.f @@ -0,0 +1,11 @@ +// rabbit3 (RV32I, 3-stage) + shared rabbit_common blocks + rabbit_cpu adapter. +// ${REPO} is expanded by Verilator / the Makefiles. +${REPO}/rtl/cores/rabbit_common/rabbit_pkg.sv +${REPO}/rtl/cores/rabbit_common/rabbit_decoder.sv +${REPO}/rtl/cores/rabbit_common/rabbit_alu.sv +${REPO}/rtl/cores/rabbit_common/rabbit_regfile.sv +${REPO}/rtl/cores/rabbit_common/rabbit_csr.sv +${REPO}/rtl/cores/rabbit_common/rabbit_execute.sv +${REPO}/rtl/cores/rabbit_common/rabbit_rvfi.sv +${REPO}/rtl/cores/rabbit3/rabbit3_core.sv +${REPO}/rtl/cores/rabbit3/rabbit_cpu.sv diff --git a/rtl/cores/rabbit3/rabbit3_core.sv b/rtl/cores/rabbit3/rabbit3_core.sv new file mode 100644 index 0000000..1d4841a --- /dev/null +++ b/rtl/cores/rabbit3/rabbit3_core.sv @@ -0,0 +1,201 @@ +// ============================================================================= +// rabbit3_core — 3-stage in-order RV32I pipeline (single hart) +// ============================================================================= +// START HERE to learn the rabbit pipelines; then read rabbit5_core.sv. +// +// cycle: 1 2 3 4 +// instr A F X W +// instr B F X W +// +// F : send pc to instruction memory +// X : instruction word arrives; decode; read registers; execute; +// send load/store to data memory <- commit point +// W : load data arrives; write register; report to RVFI +// +// Why there is no forwarding logic and no load-use stall: +// The only older instruction an instruction in X can depend on is the one in +// W. W writes the register file in the same cycle in which X reads it, and +// the register file passes the new value straight through ("write-first +// bypass", rabbit_regfile.sv). That new value already includes load data, +// because the data memory answers at the start of W. +// +// What the extra stages of rabbit5 buy instead: a shorter clock period. In +// rabbit3 one cycle must fit memory -> load align -> register bypass -> ALU +// -> data address (in rabbit5 that path is cut into separate stages). +// +// ----------------------------------------------------------------------------- +// TIMING RULES (checked in dv/formal/rabbit/timing with CORE=rabbit3) +// ----------------------------------------------------------------------------- +// R1 One instruction retires per cycle, except: +// R2 Load-use costs nothing (see above). +// R3 Redirect (taken branch, JAL, JALR, MRET, any trap) is decided in X +// and costs exactly 1 cycle (1 bubble). +// R4 Memory must answer in exactly 1 cycle (grant in the request cycle, +// data the next cycle). +// R5 Nothing else ever stalls the pipeline. +// +// So the time between two consecutive retirements is 1 or 2 cycles. +// ----------------------------------------------------------------------------- +// +// What an instruction does lives in rtl/cores/rabbit_common/ (shared with +// rabbit5): rabbit_decoder, rabbit_regfile, rabbit_execute, rabbit_rvfi. +// This file is ONLY the pipeline. +// ============================================================================= +module rabbit3_core + import rabbit_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 +); + + exec_t w_q; // X/W pipeline register: the executed instruction + logic [31:0] w_result; // its final register value (load data for loads) + logic redirect; + logic [31:0] redirect_pc; + + // =========================================================================== + // F — instruction fetch + // =========================================================================== + logic [31:0] pc_q; // address requested this cycle + + 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 (fetch_enable_i) pc_q <= pc_q + 32'd4; + end + + // =========================================================================== + // X — decode, register read, execute, data request + // =========================================================================== + logic x_valid_q; // the word arriving now is a real instruction + logic [31:0] x_pc_q; // ... fetched from this address + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + x_valid_q <= 1'b0; + x_pc_q <= '0; + end else if (redirect) begin // the word in flight is wrong-path + x_valid_q <= 1'b0; + end else begin + x_valid_q <= fetch_enable_i; + x_pc_q <= pc_q; + end + end + + decoded_t x_dec; + rabbit_decoder u_decoder (.instr_i(instr_rdata_i), .dec_o(x_dec)); + + // Register file: read in X, written in W. The write-first bypass inside + // is this core's entire forwarding network. + logic [31:0] x_rs1_val, x_rs2_val; + rabbit_regfile u_regfile ( + .clk_i, + .raddr_a_i(x_dec.rs1), .rdata_a_o(x_rs1_val), + .raddr_b_i(x_dec.rs2), .rdata_b_o(x_rs2_val), + .we_i(w_q.valid && w_q.writes_rd), .waddr_i(w_q.rd), .wdata_i(w_result) + ); + + exec_t x_res; + rabbit_execute #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute ( + .clk_i, .rst_ni, + .valid_i (x_valid_q), + .pc_i (x_pc_q), + .instr_i (instr_rdata_i), + .dec_i (x_dec), + .rs1_i (x_rs1_val), + .rs2_i (x_rs2_val), + .res_o (x_res), + .redirect_o (redirect), + .redirect_pc_o(redirect_pc) + ); + + // the data access leaves directly from X; the answer arrives in W (rule R4) + assign data_req_o = x_res.valid && (x_res.is_load || x_res.is_store); + assign data_we_o = x_res.is_store; + assign data_addr_o = {x_res.addr[31:2], 2'b00}; + assign data_be_o = x_res.mem_be; + assign data_wdata_o = x_res.mem_wdata; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) w_q <= '0; + else w_q <= x_res; + end + + // =========================================================================== + // W — load data arrives, write the register file, report to RVFI + // =========================================================================== + assign w_result = w_q.is_load ? lsu_load_value(w_q.funct3, w_q.addr[1:0], data_rdata_i) + : w_q.result; + + rabbit_rvfi u_rvfi ( + .clk_i, .rst_ni, + .retire_i(w_q), .rd_wdata_i(w_result), .mem_rdata_i(data_rdata_i), + .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 + ); + +`ifndef SYNTHESIS + always_ff @(posedge clk_i or negedge rst_ni) begin + if (rst_ni) begin + if (instr_req_o && !instr_gnt_i) $error("rabbit3: instruction memory must grant immediately (rule R4)"); + if (data_req_o && !data_gnt_i) $error("rabbit3: data memory must grant immediately (rule R4)"); + end + end +`endif + + logic unused; + assign unused = ^{instr_rvalid_i, data_rvalid_i, irq_i}; + +endmodule diff --git a/rtl/cores/rabbit3/rabbit_cpu.sv b/rtl/cores/rabbit3/rabbit_cpu.sv new file mode 100644 index 0000000..ca109e4 --- /dev/null +++ b/rtl/cores/rabbit3/rabbit_cpu.sv @@ -0,0 +1,54 @@ +// rabbit_cpu adapter for rabbit3 (our own 3-stage RV32I core). +// See rtl/cores/README.md for the port contract. rabbit5 needs memories that +// grant immediately and answer one cycle later (rabbit3_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 +); + rabbit3_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/cores/rabbit5/README.md b/rtl/cores/rabbit5/README.md index 23568ea..324b6bf 100644 --- a/rtl/cores/rabbit5/README.md +++ b/rtl/cores/rabbit5/README.md @@ -17,27 +17,31 @@ IF ──► ID ──► EX ──► MEM ──► WB | 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` | +| `hello` firmware in the SoC | PASS, 3958 cycles (rabbit3: 3145, CV32E40P: 3450 with 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 CORE=rabbit5` | +| Timing properties T1–T3 (ours, beyond riscv-formal) | PASS (BMC depth 24) + all covers reached | `make formal CORE=rabbit5` | | 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` | +| Size (Yosys generic synthesis, core + adapter) | ≈ 11.1 k cells | `make gls-netlist CORE=rabbit5` | -Whole formal suite: ~35 s on a 22-core machine. +> Correction (2026-11-06): the first version of the timing testbench declared +> its free inputs with `(* anyseq *)`, which the slang frontend silently +> ignores — the instruction stream became a "don't care" constant instead of a +> real input, so the first T1–T3 "PASS" was weaker than claimed. Found while +> bringing up rabbit3 (an impossible counterexample); fixed by making the free +> values top-level inputs, then re-proven and re-mutation-tested on both cores. -## Reading order (≈ 1,000 lines of RTL, comments included) +## Reading order + +Read **rabbit3 first** (`../rabbit3/README.md`): same blocks, simpler pipeline. +Then: | # | 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 | +| 1 | `../rabbit_common/` (see its README) | ~800 | the shared blocks: decode, ALU, regfile, CSRs, `rabbit_execute`, RVFI | +| 2 | `rabbit5_core.sv` | ~280 | **the pipeline only** — start with the TIMING RULES header; compare with `rabbit3_core.sv` | +| 3 | `../../../dv/formal/rabbit/timing/rabbit_timing_tb.sv` | ~170 | the timing properties T1–T3 (same file for every core) | +| 4 | `../../../dv/formal/rabbit/wrapper.sv`, `checks.cfg` | | how riscv-formal sees the core | ## The timing model (rules R1–R5, in `rabbit5_core.sv`) @@ -65,7 +69,7 @@ Design choices you may want to change: 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*. +- [ ] Break something on purpose (e.g. swap the MEM/WB priority in `forward()`) and watch which formal check fails (`make formal CORE=rabbit5`). 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 diff --git a/rtl/cores/rabbit5/core.mk b/rtl/cores/rabbit5/core.mk index 1f53cc2..078cc91 100644 --- a/rtl/cores/rabbit5/core.mk +++ b/rtl/cores/rabbit5/core.mk @@ -3,3 +3,9 @@ CORE_MARCH := rv32i_zicsr CORE_MABI := ilp32 # Our own RTL: no warning suppressions. CORE_VERILATOR_FLAGS := + +# Timing model of this core (rabbit5_core.sv, TIMING RULES). The formal +# timing properties in dv/formal/rabbit/timing check the core against these. +TIMING_FIRST_RETIRE := 5 +TIMING_REDIRECT_GAP := 3 +TIMING_LOADUSE_GAP := 2 diff --git a/rtl/cores/rabbit5/files.f b/rtl/cores/rabbit5/files.f index 0f11a6b..9f897ef 100644 --- a/rtl/cores/rabbit5/files.f +++ b/rtl/cores/rabbit5/files.f @@ -1,8 +1,11 @@ -// 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 +// rabbit5 (RV32I, 5-stage) + shared rabbit_common blocks + rabbit_cpu adapter. +// ${REPO} is expanded by Verilator / the Makefiles. +${REPO}/rtl/cores/rabbit_common/rabbit_pkg.sv +${REPO}/rtl/cores/rabbit_common/rabbit_decoder.sv +${REPO}/rtl/cores/rabbit_common/rabbit_alu.sv +${REPO}/rtl/cores/rabbit_common/rabbit_regfile.sv +${REPO}/rtl/cores/rabbit_common/rabbit_csr.sv +${REPO}/rtl/cores/rabbit_common/rabbit_execute.sv +${REPO}/rtl/cores/rabbit_common/rabbit_rvfi.sv ${REPO}/rtl/cores/rabbit5/rabbit5_core.sv ${REPO}/rtl/cores/rabbit5/rabbit_cpu.sv diff --git a/rtl/cores/rabbit5/rabbit5_core.sv b/rtl/cores/rabbit5/rabbit5_core.sv index 2333640..4d9b05d 100644 --- a/rtl/cores/rabbit5/rabbit5_core.sv +++ b/rtl/cores/rabbit5/rabbit5_core.sv @@ -1,5 +1,5 @@ // ============================================================================= -// rabbit5_core — 5-stage in-order RV32I pipeline (v0, single hart) +// rabbit5_core — 5-stage in-order RV32I pipeline (single hart) // ============================================================================= // // cycle: 1 2 3 4 5 6 @@ -13,7 +13,8 @@ // WB : load data arrives; write register; report to RVFI // // ----------------------------------------------------------------------------- -// TIMING RULES (the whole timing model of v0 — checked in dv/formal/rabbit5/timing) +// TIMING RULES (checked in dv/formal/rabbit/timing with CORE=rabbit5; +// the numbers are declared in core.mk) // ----------------------------------------------------------------------------- // R1 One instruction retires per cycle, except: // R2 Load-use: if an instruction reads the register loaded by the load @@ -30,12 +31,18 @@ // cycles and depends only on those two instructions. // ----------------------------------------------------------------------------- // +// This file is ONLY the pipeline: stage registers, hazards, forwarding. +// What an instruction does is in rtl/cores/rabbit_common/ (shared with rabbit3): +// rabbit_decoder (ID), rabbit_regfile, rabbit_execute (EX, incl. CSRs/traps), +// rabbit_rvfi (reporting). Compare with rabbit3_core.sv to see what two +// extra stages cost and buy. +// // 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::*; + import rabbit_pkg::*; #( parameter logic [31:0] BOOT_ADDR = 32'h0000_0080, parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000, @@ -89,43 +96,26 @@ module rabbit5_core ); // =========================================================================== - // Pipeline registers. Each struct is "what this stage needs to know". + // Pipeline registers // =========================================================================== - - // ID/EX + // ID/EX: a decoded instruction plus the register values read in ID 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] rs1_val; // EX may replace these by newer values (forwarding) 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; + ex_stage_t ex_q; // ID/EX + exec_t mem_q; // EX/MEM : result of rabbit_execute + exec_t wb_q; // MEM/WB : same record, one stage later logic redirect; // EX changes control flow this cycle logic [31:0] redirect_pc; logic stall; // ID must wait one cycle (load-use) + logic [31:0] wb_result; // final register value of the instruction in WB // =========================================================================== // IF — instruction fetch @@ -177,29 +167,17 @@ module rabbit5_core end decoded_t id_dec; - rabbit5_decoder u_decoder (.instr_i(id_instr), .dec_o(id_dec)); + rabbit_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; + // Register file: read in ID, written in WB (write-first bypass inside) logic [31:0] id_rs1_val, id_rs2_val; - - rabbit5_regfile u_regfile ( + rabbit_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) + .we_i(wb_q.valid && wb_q.writes_rd), .waddr_i(wb_q.rd), .wdata_i(wb_result) ); - // =========================================================================== - // 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; @@ -221,7 +199,11 @@ module rabbit5_core end end - // ---- forwarding: use the newest value of a register ----------------------- + // =========================================================================== + // EX — forwarding + rabbit_execute + // =========================================================================== + // The values read in ID may be out of date: an older instruction that is + // now in MEM or WB has not written the register file yet. Use the newest. // 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); @@ -230,252 +212,53 @@ module rabbit5_core 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 ( + exec_t ex_res; + rabbit_execute #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute ( .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) + .valid_i (ex_q.valid), + .pc_i (ex_q.pc), + .instr_i (ex_q.instr), + .dec_i (ex_q.dec), + .rs1_i (forward(ex_q.dec.rs1, ex_q.rs1_val)), + .rs2_i (forward(ex_q.dec.rs2, ex_q.rs2_val)), + .res_o (ex_res), + .redirect_o (redirect), + .redirect_pc_o(redirect_pc) ); - // ---- 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 + else mem_q <= ex_res; end // =========================================================================== - // MEM — issue the data access (answer arrives in WB, rule R4) + // MEM — issue the data access (the 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 + assign data_be_o = mem_q.mem_be; + assign data_wdata_o = mem_q.mem_wdata; - // ---- 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 + if (!rst_ni) wb_q <= '0; + else wb_q <= mem_q; end // =========================================================================== - // WB — load data arrives, write the register file + // WB — load data arrives, write the register file, report to RVFI // =========================================================================== - 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 ? lsu_load_value(wb_q.funct3, wb_q.addr[1:0], data_rdata_i) + : wb_q.result; - 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; + rabbit_rvfi u_rvfi ( + .clk_i, .rst_ni, + .retire_i(wb_q), .rd_wdata_i(wb_result), .mem_rdata_i(data_rdata_i), + .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 + ); // =========================================================================== // Simulation-only check of rule R4 (the memory contract) @@ -489,8 +272,8 @@ module rabbit5_core end `endif - // Inputs that v0 does not use (kept so the port list matches rabbit_cpu) + // Inputs that are not used (kept so the port list matches rabbit_cpu) logic unused; - assign unused = ^{instr_rvalid_i, data_rvalid_i, irq_i, wb_q.store_data}; + assign unused = ^{instr_rvalid_i, data_rvalid_i, irq_i}; endmodule diff --git a/rtl/cores/rabbit_common/README.md b/rtl/cores/rabbit_common/README.md new file mode 100644 index 0000000..986c3cc --- /dev/null +++ b/rtl/cores/rabbit_common/README.md @@ -0,0 +1,37 @@ +# rabbit_common — blocks shared by every rabbit core + +Everything an instruction *does* lives here. A rabbit core +(`../rabbit3/rabbit3_core.sv`, `../rabbit5/rabbit5_core.sv`) only decides +*when* things happen: pipeline registers, bubbles, stalls and forwarding. + +| File | Kind | What it does | +|---|---|---| +| `rabbit_pkg.sv` | package | opcodes, CSR numbers, cause codes; `decoded_t` (output of decode) and `exec_t` (output of execute); helper functions for branches and load/store byte lanes | +| `rabbit_decoder.sv` | combinational | 32 instruction bits → `decoded_t`; marks unsupported encodings as illegal | +| `rabbit_alu.sv` | combinational | the ten RV32I ALU operations | +| `rabbit_regfile.sv` | state | 31 × 32-bit registers (x0 = 0), 2 read ports, 1 write port, write-first bypass | +| `rabbit_csr.sv` | state | machine-mode CSRs, counters, trap entry, MRET | +| `rabbit_execute.sv` | combinational + CSR state | ALU operands, branch/jump decision, exceptions, CSR access, next pc → `exec_t` + redirect | +| `rabbit_rvfi.sv` | small state | turns the retiring `exec_t` into the RVFI port used by formal verification | + +``` + instruction word + │ + rabbit_decoder ──► decoded_t ──┐ + │ operand values (from the + rabbit_regfile ──► rs1, rs2 ───┤◄──── pipeline: bypass / forwarding) + ▼ + rabbit_execute ──► redirect, redirect_pc (to fetch) + (ALU, branch, │ + CSR, traps) ▼ + exec_t ──► memory request + │ (from X or MEM) + ▼ + retirement: load data, regfile write, + rabbit_rvfi +``` + +Rules for this directory: +- nothing here may know how many stages a core has; +- a change here affects every core → run `make formal CORE=rabbit3` **and** + `make formal CORE=rabbit5` (CI does both). diff --git a/rtl/cores/rabbit5/rabbit5_alu.sv b/rtl/cores/rabbit_common/rabbit_alu.sv similarity index 88% rename from rtl/cores/rabbit5/rabbit5_alu.sv rename to rtl/cores/rabbit_common/rabbit_alu.sv index 8a0ff51..1bc0d85 100644 --- a/rtl/cores/rabbit5/rabbit5_alu.sv +++ b/rtl/cores/rabbit_common/rabbit_alu.sv @@ -1,8 +1,8 @@ // ============================================================================= -// rabbit5_alu — RV32I integer ALU (pure combinational, one cycle) +// rabbit_alu — RV32I integer ALU (pure combinational, one cycle) // ============================================================================= -module rabbit5_alu - import rabbit5_pkg::*; +module rabbit_alu + import rabbit_pkg::*; ( input alu_op_e op_i, input logic [31:0] a_i, diff --git a/rtl/cores/rabbit5/rabbit5_csr.sv b/rtl/cores/rabbit_common/rabbit_csr.sv similarity index 97% rename from rtl/cores/rabbit5/rabbit5_csr.sv rename to rtl/cores/rabbit_common/rabbit_csr.sv index 9328db2..6cd4ae7 100644 --- a/rtl/cores/rabbit5/rabbit5_csr.sv +++ b/rtl/cores/rabbit_common/rabbit_csr.sv @@ -1,5 +1,5 @@ // ============================================================================= -// rabbit5_csr — machine-mode CSRs and trap state (v0: no interrupts) +// rabbit_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 @@ -9,8 +9,8 @@ // mscratch, mepc, mcause, mtval, mcycle[h], minstret[h], mhartid. // Any other address -> illegal instruction (reported back to EX). // ============================================================================= -module rabbit5_csr - import rabbit5_pkg::*; +module rabbit_csr + import rabbit_pkg::*; #( parameter logic [31:0] MTVEC_RESET = 32'h0, parameter logic [31:0] HART_ID = 32'h0 diff --git a/rtl/cores/rabbit5/rabbit5_decoder.sv b/rtl/cores/rabbit_common/rabbit_decoder.sv similarity index 98% rename from rtl/cores/rabbit5/rabbit5_decoder.sv rename to rtl/cores/rabbit_common/rabbit_decoder.sv index c5e52c8..2a4403f 100644 --- a/rtl/cores/rabbit5/rabbit5_decoder.sv +++ b/rtl/cores/rabbit_common/rabbit_decoder.sv @@ -1,12 +1,12 @@ // ============================================================================= -// rabbit5_decoder — instruction bits -> decoded_t (pure combinational) +// rabbit_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::*; +module rabbit_decoder + import rabbit_pkg::*; ( input logic [31:0] instr_i, output decoded_t dec_o diff --git a/rtl/cores/rabbit_common/rabbit_execute.sv b/rtl/cores/rabbit_common/rabbit_execute.sv new file mode 100644 index 0000000..4796ecb --- /dev/null +++ b/rtl/cores/rabbit_common/rabbit_execute.sv @@ -0,0 +1,149 @@ +// ============================================================================= +// rabbit_execute — the execute stage logic, shared by every rabbit core +// ============================================================================= +// Input : one decoded instruction and its two operand values. Getting the +// *right* operand values (forwarding, stalls) is the pipeline's job, +// not this module's. +// Output: an exec_t record (what the instruction did) and, if control flow +// changes, a redirect. +// +// This is the commit point of every rabbit core: all exceptions are found +// here and all CSR state changes here. An instruction that leaves execute +// without a trap is guaranteed to retire. +// +// operands ─► ALU ─────────────► result / load-store address +// └─► branch unit ─────► taken? target? +// └─► CSR unit ────────► old CSR value, trap entry, MRET +// └─► exception check ─► trap? cause? +// └► next_pc, redirect +// ============================================================================= +module rabbit_execute + import rabbit_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, + + input logic valid_i, + input logic [31:0] pc_i, + input logic [31:0] instr_i, + input decoded_t dec_i, + input logic [31:0] rs1_i, // operand values, already up to date + input logic [31:0] rs2_i, + + output exec_t res_o, + output logic redirect_o, // control flow changes: fetch from redirect_pc_o + output logic [31:0] redirect_pc_o +); + + // ---- ALU ------------------------------------------------------------------ + logic [31:0] alu_a, alu_b, alu_y; + always_comb begin + unique case (dec_i.opa) + OPA_RS1: alu_a = rs1_i; + OPA_PC : alu_a = pc_i; + default: alu_a = 32'b0; + endcase + alu_b = (dec_i.opb == OPB_RS2) ? rs2_i : dec_i.imm; + end + + rabbit_alu u_alu (.op_i(dec_i.alu_op), .a_i(alu_a), .b_i(alu_b), .y_o(alu_y)); + + // ---- branches and jumps ----------------------------------------------------- + logic taken; + logic [31:0] jump_target; + assign taken = dec_i.is_jal || dec_i.is_jalr || + (dec_i.is_branch && branch_taken(dec_i.funct3, rs1_i, rs2_i)); + assign jump_target = dec_i.is_jalr ? ((rs1_i + dec_i.imm) & ~32'd1) + : (pc_i + dec_i.imm); + + // ---- exceptions --------------------------------------------------------------- + logic csr_illegal; + logic target_misaligned, mem_misaligned; + assign target_misaligned = taken && (jump_target[1:0] != 2'b00); + assign mem_misaligned = (dec_i.is_load || dec_i.is_store) && + lsu_misaligned(dec_i.funct3[1:0], alu_y[1:0]); + + logic trap; + logic [31:0] trap_cause, trap_tval; + always_comb begin + trap = 1'b1; + trap_tval = 32'b0; + if (dec_i.illegal || csr_illegal) begin trap_cause = CAUSE_ILLEGAL_INSN; trap_tval = instr_i; end + else if (dec_i.is_ecall) trap_cause = CAUSE_ECALL_M; + else if (dec_i.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 = dec_i.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 && valid_i; + 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 = (dec_i.funct3[1:0] == 2'b01) || (dec_i.rs1 != 5'd0); + + rabbit_csr #(.MTVEC_RESET(MTVEC_RESET), .HART_ID(HART_ID)) u_csr ( + .clk_i, .rst_ni, + .csr_valid_i (valid_i && dec_i.is_csr), + .csr_addr_i (instr_i[31:20]), + .csr_op_i (dec_i.funct3[1:0]), + .csr_write_i (csr_write_req), + .csr_src_i (dec_i.funct3[2] ? dec_i.imm : rs1_i), + .csr_rdata_o (csr_rdata), + .csr_illegal_o(csr_illegal), + .trap_i (trap), + .trap_cause_i (trap_cause), + .trap_pc_i (pc_i), + .trap_tval_i (trap_tval), + .mret_i (valid_i && dec_i.is_mret), + .instret_i (valid_i && !trap), + .mtvec_o (mtvec), + .mepc_o (mepc) + ); + + // ---- next pc and redirect ------------------------------------------------------ + logic [31:0] next_pc; + always_comb begin + if (trap) next_pc = mtvec; + else if (dec_i.is_mret) next_pc = mepc; + else if (taken) next_pc = jump_target; + else next_pc = pc_i + 32'd4; + end + assign redirect_o = valid_i && (trap || dec_i.is_mret || taken); + assign redirect_pc_o = next_pc; + + // ---- the result record ------------------------------------------------------------ + always_comb begin + res_o = '0; + res_o.valid = valid_i; + res_o.pc = pc_i; + res_o.instr = instr_i; + res_o.next_pc = next_pc; + res_o.trap = trap; + res_o.writes_rd = dec_i.writes_rd && !trap; // a trap has no side effects + res_o.rd = dec_i.rd; + unique case (dec_i.res) + RES_PC4: res_o.result = pc_i + 32'd4; + RES_CSR: res_o.result = csr_rdata; + default: res_o.result = alu_y; + endcase + res_o.is_load = dec_i.is_load && !trap; + res_o.is_store = dec_i.is_store && !trap; + res_o.funct3 = dec_i.funct3; + res_o.addr = alu_y; + res_o.mem_be = lsu_byte_enable(dec_i.funct3[1:0], alu_y[1:0]); + res_o.mem_wdata = lsu_store_lanes(dec_i.funct3[1:0], rs2_i); + res_o.rs1_addr = dec_i.uses_rs1 ? dec_i.rs1 : 5'd0; + res_o.rs2_addr = dec_i.uses_rs2 ? dec_i.rs2 : 5'd0; + res_o.rs1_val = dec_i.uses_rs1 ? rs1_i : 32'd0; + res_o.rs2_val = dec_i.uses_rs2 ? rs2_i : 32'd0; + end + +endmodule diff --git a/rtl/cores/rabbit5/rabbit5_pkg.sv b/rtl/cores/rabbit_common/rabbit_pkg.sv similarity index 51% rename from rtl/cores/rabbit5/rabbit5_pkg.sv rename to rtl/cores/rabbit_common/rabbit_pkg.sv index 6533d6d..92b1aa7 100644 --- a/rtl/cores/rabbit5/rabbit5_pkg.sv +++ b/rtl/cores/rabbit_common/rabbit_pkg.sv @@ -1,18 +1,12 @@ // ============================================================================= -// rabbit5_pkg — shared types for the rabbit5 core +// rabbit_pkg — types, constants and small helper functions shared by every +// rabbit core (rabbit3, rabbit5, ...) // ============================================================================= -// 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. +// Everything here is "a fact about RISC-V" (opcodes, CSR numbers, cause codes) +// or a stage-independent helper. Nothing here knows how many pipeline stages a +// core has — that lives only in rabbitN_core.sv. // ============================================================================= -package rabbit5_pkg; +package rabbit_pkg; // --------------------------------------------------------------------------- // RV32I major opcodes (instruction bits [6:0]) @@ -52,7 +46,7 @@ package rabbit5_pkg; // --------------------------------------------------------------------------- // Decoded instruction: everything later stages need to know, produced once - // by rabbit5_decoder in ID. + // by rabbit_decoder. // --------------------------------------------------------------------------- typedef struct packed { logic illegal; // not a supported instruction -> trap in EX @@ -98,6 +92,90 @@ package rabbit5_pkg; // misa: MXL=1 (32-bit), extension I only localparam logic [31:0] MISA_VALUE = 32'h4000_0100; + // --------------------------------------------------------------------------- + // exec_t: everything known about an instruction once it has been executed. + // Produced by rabbit_execute, then simply carried to retirement: + // rabbit3: X -> W rabbit5: EX -> MEM -> WB + // --------------------------------------------------------------------------- + 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; // trapped: no register write, no memory access + logic writes_rd; + logic [4:0] rd; + logic [31:0] result; // ALU / link / CSR value (loads: replaced at retirement) + logic is_load; + logic is_store; + logic [2:0] funct3; // load size and sign + logic [31:0] addr; // byte address of the load/store + logic [3:0] mem_be; // byte enables within the addressed word + logic [31:0] mem_wdata; // store data, already placed on the right byte lanes + logic [4:0] rs1_addr; // operands actually used (for RVFI only) + logic [4:0] rs2_addr; + logic [31:0] rs1_val; + logic [31:0] rs2_val; + } exec_t; + + // --------------------------------------------------------------------------- + // Helper functions (pure combinational) + // --------------------------------------------------------------------------- + + // Branch condition for BEQ/BNE/BLT/BGE/BLTU/BGEU (funct3 selects) + function automatic logic branch_taken(input logic [2:0] funct3, + input logic [31:0] a, input logic [31:0] b); + unique case (funct3) + 3'b000 : return a == b; // BEQ + 3'b001 : return a != b; // BNE + 3'b100 : return $signed(a) < $signed(b); // BLT + 3'b101 : return $signed(a) >= $signed(b); // BGE + 3'b110 : return a < b; // BLTU + 3'b111 : return a >= b; // BGEU + default: return 1'b0; + endcase + endfunction + + // Load/store size from funct3[1:0]: 00 byte, 01 half word, 10 word + function automatic logic lsu_misaligned(input logic [1:0] size, input logic [1:0] offset); + unique case (size) + 2'b00 : return 1'b0; + 2'b01 : return offset[0]; + default: return offset != 2'b00; + endcase + endfunction + + function automatic logic [3:0] lsu_byte_enable(input logic [1:0] size, input logic [1:0] offset); + unique case (size) + 2'b00 : return 4'b0001 << offset; + 2'b01 : return 4'b0011 << offset; + default: return 4'b1111; + endcase + endfunction + + // Replicate store data so every byte lane carries the right byte + function automatic logic [31:0] lsu_store_lanes(input logic [1:0] size, input logic [31:0] data); + unique case (size) + 2'b00 : return {4{data[7:0]}}; + 2'b01 : return {2{data[15:0]}}; + default: return data; + endcase + endfunction + + // Pick the loaded bytes out of the memory word and sign/zero-extend them + function automatic logic [31:0] lsu_load_value(input logic [2:0] funct3, input logic [1:0] offset, + input logic [31:0] word); + logic [31:0] w; + w = word >> {offset, 3'b000}; + unique case (funct3) + 3'b000 : return {{24{w[7]}}, w[7:0]}; // LB + 3'b001 : return {{16{w[15]}}, w[15:0]}; // LH + 3'b100 : return {24'b0, w[7:0]}; // LBU + 3'b101 : return {16'b0, w[15:0]}; // LHU + default: return w; // LW + endcase + endfunction + // Exception cause codes (mcause) localparam logic [31:0] CAUSE_INSN_MISALIGNED = 32'd0; localparam logic [31:0] CAUSE_ILLEGAL_INSN = 32'd2; diff --git a/rtl/cores/rabbit5/rabbit5_regfile.sv b/rtl/cores/rabbit_common/rabbit_regfile.sv similarity index 92% rename from rtl/cores/rabbit5/rabbit5_regfile.sv rename to rtl/cores/rabbit_common/rabbit_regfile.sv index e8bac8c..39816e8 100644 --- a/rtl/cores/rabbit5/rabbit5_regfile.sv +++ b/rtl/cores/rabbit_common/rabbit_regfile.sv @@ -1,12 +1,12 @@ // ============================================================================= -// rabbit5_regfile — 32 x 32-bit registers, 2 read ports, 1 write port +// rabbit_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 ( +module rabbit_regfile ( input logic clk_i, input logic [4:0] raddr_a_i, output logic [31:0] rdata_a_o, diff --git a/rtl/cores/rabbit_common/rabbit_rvfi.sv b/rtl/cores/rabbit_common/rabbit_rvfi.sv new file mode 100644 index 0000000..26aa4e2 --- /dev/null +++ b/rtl/cores/rabbit_common/rabbit_rvfi.sv @@ -0,0 +1,72 @@ +// ============================================================================= +// rabbit_rvfi — report each retired instruction on the RVFI port +// ============================================================================= +// RVFI (RISC-V Formal Interface) is how riscv-formal and our timing properties +// see the core: one record per retired instruction, in program order. +// Every rabbit core retires from an exec_t record plus, for loads, the data +// that just came back from memory. +// ============================================================================= +module rabbit_rvfi + import rabbit_pkg::*; +( + input logic clk_i, + input logic rst_ni, + + input exec_t retire_i, // the instruction retiring this cycle (if .valid) + input logic [31:0] rd_wdata_i, // its final register value (load data for loads) + input logic [31:0] mem_rdata_i, // the raw memory word (loads) + + 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 +); + logic [63:0] order_q; + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) order_q <= '0; + else if (retire_i.valid) order_q <= order_q + 64'd1; + end + + assign rvfi_valid = retire_i.valid; + assign rvfi_order = order_q; + assign rvfi_insn = retire_i.instr; + assign rvfi_trap = retire_i.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 = retire_i.rs1_addr; + assign rvfi_rs2_addr = retire_i.rs2_addr; + assign rvfi_rs1_rdata = retire_i.rs1_val; + assign rvfi_rs2_rdata = retire_i.rs2_val; + assign rvfi_rd_addr = retire_i.writes_rd ? retire_i.rd : 5'd0; + assign rvfi_rd_wdata = retire_i.writes_rd ? rd_wdata_i : 32'd0; + assign rvfi_pc_rdata = retire_i.pc; + assign rvfi_pc_wdata = retire_i.next_pc; + assign rvfi_mem_addr = {retire_i.addr[31:2], 2'b00}; + assign rvfi_mem_rmask = retire_i.is_load ? retire_i.mem_be : 4'b0; + assign rvfi_mem_wmask = retire_i.is_store ? retire_i.mem_be : 4'b0; + assign rvfi_mem_rdata = mem_rdata_i; + assign rvfi_mem_wdata = retire_i.is_store ? retire_i.mem_wdata : 32'd0; + + // result/funct3 are already folded into rd_wdata_i by the pipeline + logic unused; + assign unused = ^{retire_i.result, retire_i.funct3}; +endmodule