rabbit_common + rabbit3: shared core library and a 3-stage RV32I core

.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

.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*/

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

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
 

dv/formal/README.md

@@ -1,36 +1,66 @@
 # 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>/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>/core_flat.v`).
 2. `genchecks.py` expects `<riscv-formal>/cores/<core>/`; the Makefile builds a
-   small mirror in `build/` (symlinks to the submodule), so the submodule is
-   never modified.
+   small mirror in `build/<core>/` (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.
+### 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
 

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 <riscv-formal>/cores/<core>/, 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

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: <check>  [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);