abmajith · Nov 7, 2026 · Nov 7, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -26,20 +26,20 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [cv32e40p, cve2, ibex, rabbit3, rabbit5]
+        config: [cv32e40p, cve2, ibex, rabbit3, rabbit5, rabbit3_rv32i, rabbit5_rv32i]
     steps:
       - uses: actions/checkout@v4
         with: { submodules: recursive }
-      - run: verilator --version && make lint CORE=${{ matrix.core }}
+      - run: verilator --version && make lint CONFIG=${{ matrix.config }}
 
   soc-sim:
-    # One job per (core, program). Add cores here as rtl/cores/<name>/ adapters land.
+    # One job per (configuration, program); configurations are the files in configs/.
     runs-on: ubuntu-24.04
     container: { image: "verilator/verilator:v5.054", options: --entrypoint "" }
     strategy:
       fail-fast: false
       matrix:
-        core: [cv32e40p, cve2, ibex, rabbit3, rabbit5]
+        config: [cv32e40p, cve2, ibex, rabbit3, rabbit5, rabbit3_rv32i, rabbit5_rv32i]
         # irq: interrupt self-test; cv32e40p is the reference the rabbits must match
         prog: [hello, irq, muldiv]
     steps:
@@ -48,14 +48,14 @@ jobs:
       - uses: actions/checkout@v4
         with: { submodules: recursive }
       - uses: astral-sh/setup-uv@v6
-      - run: make soc-sim CORE=${{ matrix.core }} PROG=${{ matrix.prog }}
+      - run: make soc-sim CONFIG=${{ matrix.config }} PROG=${{ matrix.prog }}
       - uses: actions/upload-artifact@v4
         if: always()
         with:
-          name: soc-${{ matrix.core }}-${{ matrix.prog }}
+          name: soc-${{ matrix.config }}-${{ matrix.prog }}
           path: |
             dv/cocotb/soc/results.xml
-            sw/baremetal/build/${{ matrix.core }}/${{ matrix.prog }}/${{ matrix.prog }}.dis
+            sw/baremetal/build/${{ matrix.config }}/${{ matrix.prog }}/${{ matrix.prog }}.dis
 
   ip-test:
     runs-on: ubuntu-24.04

diff --git a/.github/workflows/deep-verify.yml b/.github/workflows/deep-verify.yml
@@ -2,8 +2,8 @@ name: deep-verify
 
 # Heavy verification, started by hand: GitHub -> Actions -> "deep-verify" ->
 # "Run workflow" (choose what), or locally with tools/check_all.sh.
-#   formal   riscv-formal + timing properties + muldiv unit proof, both rabbit cores (~10 min)
-#   gls      firmware on the gate-level netlists of rabbit3 / rabbit5 (~4 min)
+#   formal   riscv-formal + timing properties + muldiv unit proof, every rabbit configuration (~10 min)
+#   gls      firmware on the gate-level netlists of the rabbit configurations (~4 min)
 #   mutants  plant known bugs, check each is caught (~45 min)
 #   all      everything
 on:
@@ -20,8 +20,8 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # riscv-formal (53 checks, RV32IM) + timing properties + the multiply/divide
-  # unit proof (dv/formal/rabbit/muldiv), for each of our own cores.
+  # riscv-formal (53 checks with M, 45 without) + timing properties + the multiply/divide
+  # unit proof (dv/formal/rabbit/muldiv), for each rabbit configuration.
   formal:
     if: ${{ inputs.what == 'all' || inputs.what == 'formal' }}
     runs-on: ubuntu-24.04
@@ -30,40 +30,40 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [rabbit3, rabbit5]
+        config: [rabbit3, rabbit5, rabbit3_rv32i, rabbit5_rv32i]
     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 CORE=${{ matrix.core }}
+      - run: make formal CONFIG=${{ matrix.config }}
       - uses: actions/upload-artifact@v4
         if: failure()
         with:
-          name: formal-results-${{ matrix.core }}
+          name: formal-results-${{ matrix.config }}
           path: |
-            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
+            dv/formal/rabbit/build/${{ matrix.config }}/riscv-formal/cores/*/checks/*/logfile.txt
+            dv/formal/rabbit/build/${{ matrix.config }}/riscv-formal/cores/*/checks/*/engine_0/*.vcd
+            dv/formal/rabbit/build/${{ matrix.config }}/timing_*/logfile.txt
+            dv/formal/rabbit/build/${{ matrix.config }}/timing_*/engine_0/*.vcd
 
   # Gate-level smoke test: Yosys builds the netlist, the pinned Verilator image runs it.
   gls-netlist:
     if: ${{ inputs.what == 'all' || inputs.what == 'gls' }}
     runs-on: ubuntu-24.04
     strategy:
       matrix:
-        core: [rabbit3, rabbit5]
+        config: [rabbit3, rabbit5, rabbit3_rv32i, rabbit5_rv32i]
     steps:
       - uses: actions/checkout@v4
       - uses: YosysHQ/setup-oss-cad-suite@v3
         with: { version: "2026-11-04" }
-      - run: make gls-netlist CORE=${{ matrix.core }}
+      - run: make gls-netlist CONFIG=${{ matrix.config }}
       - uses: actions/upload-artifact@v4
         with:
-          name: gls-netlist-${{ matrix.core }}
-          path: build/gls/${{ matrix.core }}
+          name: gls-netlist-${{ matrix.config }}
+          path: build/gls/${{ matrix.config }}
 
   gls-smoke:
     needs: gls-netlist
@@ -72,24 +72,24 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [rabbit3, rabbit5]
+        config: [rabbit3, rabbit5, rabbit3_rv32i, rabbit5_rv32i]
     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-${{ matrix.core }}
-          path: build/gls/${{ matrix.core }}
+          name: gls-netlist-${{ matrix.config }}
+          path: build/gls/${{ matrix.config }}
       - run: uv sync
       - working-directory: dv/cocotb/soc
-        run: uv run make CORE=${{ matrix.core }} PROG=hello GLS=1
+        run: uv run make CONFIG=${{ matrix.config }} PROG=hello GLS=1
       - working-directory: dv/cocotb/soc
-        run: uv run make CORE=${{ matrix.core }} PROG=irq GLS=1
+        run: uv run make CONFIG=${{ matrix.config }} PROG=irq GLS=1
       - name: Run muldiv on the gate-level netlist
         working-directory: dv/cocotb/soc
-        run: uv run make CORE=${{ matrix.core }} PROG=muldiv GLS=1
+        run: uv run make CONFIG=${{ matrix.config }} PROG=muldiv GLS=1
 
   mutants:
     if: ${{ inputs.what == 'all' || inputs.what == 'mutants' }}

diff --git a/Makefile b/Makefile
@@ -1,19 +1,25 @@
 # rt-rabbit top-level entry points. Everything runs inside the uv environment.
 #
 #   make help           list targets
-#   make soc-sim        run firmware PROG on the SoC with CORE (default cv32e40p/hello)
+#   make configs        list the SoC configurations (configs/*.mk)
+#   make soc-sim        run firmware PROG on the SoC CONFIG (default cv32e40p, hello)
+#   make soc-waves      the same, and write a waveform (dump.fst)
+#   make lint           Verilator lint of the SoC CONFIG
+#   make formal         riscv-formal + timing properties (rabbit configurations)
+#   make gls-smoke      synthesize CONFIG with Yosys, run firmware PROG on the netlist
 #   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=rabbit3|rabbit5)
-#   make gls-smoke      synthesize the core with Yosys, run firmware on the netlist
-#   make ci             everything CI runs
+#   make ci             everything CI runs (for the selected CONFIG)
 #   make check-all      reproduce all rabbit checks (STAGES="quick gls formal synth mutants")
+#
+# CONFIG=<name> selects configs/<name>.mk; CORE=<core> is short for that core's
+# default configuration (see configs/README.md).
 REPO := $(abspath .)
 export REPO
-CORE ?= cv32e40p
 PROG ?= hello
 
+include mk/config.mk
+
 # hw_ip/sim targets known to pass on main. telemetry_rf and top need
 # rf_packet_framer_buffer.v, which is not on main yet (see docs/STATUS.md).
 IP_TARGETS := pwm_unit qei_unit telemetry_rx telemetry_tx wb_telemetry rf_cdc \
@@ -23,19 +29,26 @@ IP_TARGETS := pwm_unit qei_unit telemetry_rx telemetry_tx wb_telemetry rf_cdc \
 RMA_XFAIL := fifo_same_priority_interference.yaml
 
 help:
-	@sed -n '2,11p' Makefile | sed 's/^# //'
+	@sed -n '2,16p' Makefile | sed 's/^# \{0,1\}//'
+
+configs:
+	@for f in configs/*.mk; do printf '%-16s %s\n' "$$(basename $$f .mk)" "$$(head -1 $$f | sed 's/^# //')"; done
+
+# For shell scripts (tools/, asic/): eval "$(make -s config-vars CONFIG=...)"
+config-vars:
+	@echo "CONFIG='$(CONFIG)' CORE='$(CORE)' CONFIG_ISA='$(CONFIG_ISA)' CONFIG_DEFINES='$(CONFIG_DEFINES)'"
 
 sync:
 	uv sync
 
 firmware:
-	$(MAKE) -C sw/baremetal PROG=$(PROG) CORE=$(CORE)
+	$(MAKE) -C sw/baremetal PROG=$(PROG) CONFIG=$(CONFIG)
 
 soc-sim: sync
-	cd dv/cocotb/soc && uv run $(MAKE) CORE=$(CORE) PROG=$(PROG)
+	cd dv/cocotb/soc && uv run $(MAKE) CONFIG=$(CONFIG) PROG=$(PROG)
 
 soc-waves: sync
-	cd dv/cocotb/soc && uv run $(MAKE) CORE=$(CORE) PROG=$(PROG) WAVES=1
+	cd dv/cocotb/soc && uv run $(MAKE) CONFIG=$(CONFIG) PROG=$(PROG) WAVES=1
 	@echo "waveform: dv/cocotb/soc/dump.fst  (open with gtkwave or surfer)"
 
 ip-test: sync
@@ -44,48 +57,47 @@ ip-test: sync
 	  (cd hw_ip/sim && uv run $(MAKE) clean >/dev/null && uv run $(MAKE) TARGET=$$t) ; \
 	done
 
+LINT_FLAGS := --lint-only --top-module rabbit_soc_sim \
+              -f rtl/cores/$(CORE)/files.f -f rtl/soc/files.f $(CORE_VERILATOR_FLAGS) $(CONFIG_DEFINES)
 lint:
-	verilator --lint-only --top-module rabbit_soc_sim \
-	  -f rtl/cores/$(CORE)/files.f -f rtl/soc/files.f \
-	  $$(sed -n 's/^CORE_VERILATOR_FLAGS *:= *//p' rtl/cores/$(CORE)/core.mk)
+	verilator $(LINT_FLAGS)
 	@# Strict (-Wall) check, but only fail on warnings in *our* RTL, not vendor cores.
-	@! verilator --lint-only -Wall -Wno-fatal -Wno-UNUSEDSIGNAL -Wno-PINCONNECTEMPTY \
-	  --top-module rabbit_soc_sim -f rtl/cores/$(CORE)/files.f -f rtl/soc/files.f \
-	  $$(sed -n 's/^CORE_VERILATOR_FLAGS *:= *//p' rtl/cores/$(CORE)/core.mk) \
+	@! verilator $(LINT_FLAGS) -Wall -Wno-fatal -Wno-UNUSEDSIGNAL -Wno-PINCONNECTEMPTY \
 	  2>&1 | grep -E '%(Warning|Error)[^:]*: [^ ]*rtl/(soc|cores)/'
-	@echo "lint: own RTL clean"
+	@echo "lint: own RTL clean ($(CONFIG))"
 
 rma-smoke: sync
 	@set -e; for f in rma_analysis/examples/*.yaml; do \
 	  case " $(RMA_XFAIL) " in *" $$(basename $$f) "*) echo "xfail $$f"; continue;; esac; \
 	  uv run rma_analysis $$f >/dev/null && echo "ok    $$f"; \
 	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 ---------------------------------------------------------------------
+# formal works on our own cores; with a reference core CONFIG it runs rabbit5
+FORMAL_CONFIG := $(if $(filter rabbit%,$(CORE)),$(CONFIG),rabbit5)
 formal:
-	$(MAKE) -C dv/formal/rabbit CORE=$(FORMAL_CORE)
+	$(MAKE) -C dv/formal/rabbit CONFIG=$(FORMAL_CONFIG)
 
 # ---- gate-level smoke test: generic Yosys gates, zero delay ----------------------
 # Catches RTL that simulates differently from what synthesizes (latches, X,
 # initial values, simulation-only constructs) long before a real PDK flow.
-GLS_DIR := build/gls/$(CORE)
+# The configuration is baked into the netlist.
+GLS_DIR := build/gls/$(CONFIG)
 YOSYS_SLANG := $(shell yosys -p 'help read_slang' >/dev/null 2>&1 || echo -m slang)
 gls-netlist: $(GLS_DIR)/rabbit_cpu_netlist.v
 # every file in the core's files.f (incl. rabbit_common), not just rtl/cores/$(CORE)/
 GLS_SOURCES := $(shell grep -v '^//' rtl/cores/$(CORE)/files.f | sed 's|$${REPO}|$(REPO)|')
-$(GLS_DIR)/rabbit_cpu_netlist.v: $(GLS_SOURCES) rtl/cores/$(CORE)/files.f
+$(GLS_DIR)/rabbit_cpu_netlist.v: $(GLS_SOURCES) rtl/cores/$(CORE)/files.f $(CONFIG_DEPS)
 	@mkdir -p $(GLS_DIR)
 	yosys $(YOSYS_SLANG) -q -l $(GLS_DIR)/synth.log -p "read_slang \
 	    $$(grep -v '^//' rtl/cores/$(CORE)/files.f | sed 's|$${REPO}|$(REPO)|' | tr '\n' ' ') \
-	    --top rabbit_cpu -DSYNTHESIS; \
+	    --top rabbit_cpu -DSYNTHESIS $(CONFIG_DEFINES); \
 	  synth -top rabbit_cpu -flatten; tee -o $(GLS_DIR)/stat.txt stat; \
 	  write_verilog -noattr $@"
 	@grep -E '^ +[0-9]+ +cells' $(GLS_DIR)/stat.txt | head -1
 
 gls-smoke: sync gls-netlist
-	cd dv/cocotb/soc && uv run $(MAKE) CORE=$(CORE) PROG=$(PROG) GLS=1
+	cd dv/cocotb/soc && uv run $(MAKE) CONFIG=$(CONFIG) PROG=$(PROG) GLS=1
 
 ci: lint soc-sim ip-test rma-smoke
 
@@ -100,4 +112,5 @@ clean:
 	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 check-all clean
+.PHONY: help configs config-vars sync firmware soc-sim soc-waves ip-test lint rma-smoke formal \
+        gls-netlist gls-smoke ci check-all clean
diff --git a/README.md b/README.md
@@ -18,6 +18,8 @@ git clone --recursive git@github.com:abmajith/rt-rabbit.git && cd rt-rabbit
 uv sync
 make soc-sim                 # run sw/baremetal/hello on CV32E40P in Verilator
 make soc-sim CORE=rabbit5    # ... on our own core (also rabbit3; PROG=irq, PROG=muldiv)
+make configs                 # list the SoC configurations (configs/): core + options
+make soc-sim CONFIG=rabbit5_rv32i PROG=muldiv   # rabbit5 without M: MUL/DIV must trap
 make formal                  # riscv-formal + timing + muldiv proofs for rabbit5 (~25 min)
 make gls-smoke CORE=rabbit5  # same firmware on the synthesized gate netlist
 make ci                      # lint + simulation tests

diff --git a/asic/orfs/energy.sh b/asic/orfs/energy.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
-# Energy of one program on one routed core, from real switching activity.
+# Energy of one program on one routed SoC configuration, from real switching activity.
 #
-#   asic/orfs/energy.sh <core> [program] [period of the ORFS run, ns] [platform]
+#   asic/orfs/energy.sh <config> [program] [period of the ORFS run, ns] [platform]
 #   asic/orfs/energy.sh rabbit3 hello            # uses build/orfs/sky130hd/rabbit3_8.0ns
 #
-# Needs a finished asic/orfs/run.sh of that core. Steps:
+# Needs a finished asic/orfs/run.sh of that configuration. Steps:
 #  1. Yosys rebuilds every sky130 cell of the routed netlist (6_final.v) from
 #     the logic function in the cell library, so Verilator can simulate it.
 #     The cells stay separate modules: flattening would rename the routed
@@ -14,20 +14,20 @@
 #  3. OpenSTA computes power from that activity, with the wire capacitances
 #     of the layout (SPEF), at the simulation clock (10 ns = 100 MHz);
 #  4. energy = power x cycles x 10 ns.
-# Output: build/orfs/<platform>/<core>_<period>ns/energy/<program>.*
+# Output: build/orfs/<platform>/<config>_<period>ns/energy/<program>.*
 set -euo pipefail
 REPO=$(cd "$(dirname "$0")/../.." && pwd)
-CORE=${1:?usage: asic/orfs/energy.sh <core> [program] [period ns] [platform]}
+CONFIG=${1:?usage: asic/orfs/energy.sh <config> [program] [period ns] [platform]}
 PROG=${2:-hello}
 PERIOD=${3:-8.0}
 PLATFORM=${4:-sky130hd}
 SIM_PERIOD_NS=10      # the cocotb testbench clock
 IMAGE=${ORFS_IMAGE:-openroad/orfs@sha256:8b4f3942318d740ea1f73f4f895bbac150b32e41eb3b7baf7722adec6538bbcf}
 
-WORK=$REPO/build/orfs/$PLATFORM/${CORE}_${PERIOD}ns
-RES=$WORK/results/$PLATFORM/$CORE/base
+WORK=$REPO/build/orfs/$PLATFORM/${CONFIG}_${PERIOD}ns
+RES=$WORK/results/$PLATFORM/$CONFIG/base
 OUT=$WORK/energy
-[ -f "$RES/6_final.v" ] || { echo "no routed netlist: run asic/orfs/run.sh $CORE $PLATFORM $PERIOD first"; exit 1; }
+[ -f "$RES/6_final.v" ] || { echo "no routed netlist: run asic/orfs/run.sh $CONFIG $PLATFORM $PERIOD first"; exit 1; }
 mkdir -p "$OUT"
 
 case $PLATFORM in
@@ -50,10 +50,10 @@ fi
 #    One run at a time: the testbench always writes dump.fst in its folder.
 cd "$REPO/dv/cocotb/soc"
 rm -f dump.fst
-uv run make -j8 CORE="$CORE" PROG="$PROG" GLS=1 NETLIST="$OUT/rabbit_cpu_pnr.v" WAVES=1 \
-     VERILATOR_EXTRA=--trace-underscore SIM_BUILD="sim_build_${CORE}_pnr_${PLATFORM}" > "$OUT/$PROG.sim.log" 2>&1 || true
+uv run make -j8 CONFIG="$CONFIG" PROG="$PROG" GLS=1 NETLIST="$OUT/rabbit_cpu_pnr.v" WAVES=1 \
+     VERILATOR_EXTRA=--trace-underscore SIM_BUILD="sim_build_${CONFIG}_pnr_${PLATFORM}" > "$OUT/$PROG.sim.log" 2>&1 || true
 CYCLES=$(grep -oE 'finished after [0-9]+ cycles' "$OUT/$PROG.sim.log" | grep -oE '[0-9]+' || true)
-grep -q "RESULT: PASS" "$OUT/$PROG.sim.log" || { echo "$CORE/$PROG: program failed on the routed netlist, see $OUT/$PROG.sim.log"; exit 1; }
+grep -q "RESULT: PASS" "$OUT/$PROG.sim.log" || { echo "$CONFIG/$PROG: program failed on the routed netlist, see $OUT/$PROG.sim.log"; exit 1; }
 # OpenSTA's VCD reader knows 'wire' but not 'logic' (only a type label in VCD)
 fst2vcd dump.fst 2>/dev/null | sed 's/^\$var logic /$var wire /' > "$OUT/$PROG.vcd"
 rm -f dump.fst
@@ -74,7 +74,7 @@ docker run --rm -u "$(id -u):$(id -g)" -v "$REPO:$REPO" "$IMAGE" bash -c "
   openroad -no_init -exit $OUT/$PROG.power.tcl" > "$OUT/$PROG.power.log" 2>&1
 
 # 4. summary
-python3 - "$OUT/$PROG.power.log" "$CORE" "$PROG" "$CYCLES" "$SIM_PERIOD_NS" <<'EOF'
+python3 - "$OUT/$PROG.power.log" "$CONFIG" "$PROG" "$CYCLES" "$SIM_PERIOD_NS" <<'EOF'
 import re, sys
 log, core, prog, cycles, t = open(sys.argv[1]).read(), sys.argv[2], sys.argv[3], int(sys.argv[4]), float(sys.argv[5])
 ann = re.search(r"^vcd\s+(\d+)", log, re.M); un = re.search(r"^unannotated\s+(\d+)", log, re.M)