diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 096cd90..726e7d9 100644
--- 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
index b443b37..2d9e67c 100644
--- 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,23 +30,23 @@ 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:
@@ -54,16 +54,16 @@ jobs:
     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,7 +72,7 @@ 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
@@ -80,16 +80,16 @@ jobs:
       - 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
index dd2a1cc..170d193 100644
--- 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,16 +57,14 @@ 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 \
@@ -61,31 +72,32 @@ rma-smoke: sync
 	  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
index ded474e..22110aa 100644
--- 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
index 8122776..983d2fe 100755
--- 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)
diff --git a/asic/orfs/run.sh b/asic/orfs/run.sh
index fe0b1a4..8511f32 100755
--- a/asic/orfs/run.sh
+++ b/asic/orfs/run.sh
@@ -1,40 +1,42 @@
 #!/usr/bin/env bash
-# Place-and-route one core with OpenROAD-flow-scripts (Docker image), then
-# report the real longest path (with wires), area and power.
+# Place-and-route one SoC configuration's core with OpenROAD-flow-scripts
+# (Docker image), then report the real longest path (with wires), area and power.
 #
-#   asic/orfs/run.sh <core> [platform] [clock period ns]
+#   asic/orfs/run.sh <config> [platform] [clock period ns]
 #   asic/orfs/run.sh rabbit3                      # sky130hd, 8 ns
+#   asic/orfs/run.sh rabbit5_rv32i                # any file in configs/
 #   asic/orfs/run.sh ibex ihp-sg13g2 8
 #
 # Steps:
-#  1. our Yosys + slang turns the core (rtl/cores/<core>/files.f) into one
-#     plain Verilog file - the same front end for every core;
+#  1. our Yosys + slang turns the core (rtl/cores/<core>/files.f, with the
+#     configuration's defines) into one plain Verilog file - the same front
+#     end for every core;
 #  2. ORFS (inside openroad/orfs, pinned below) runs synthesis, floorplan,
 #     placement, clock tree, routing;
 #  3. the summary line comes from ORFS' final reports.
-# Output: build/orfs/<platform>/<core>_<period>ns/ (logs/, reports/, results/)
+# Output: build/orfs/<platform>/<config>_<period>ns/ (logs/, reports/, results/)
 set -euo pipefail
 REPO=$(cd "$(dirname "$0")/../.." && pwd)
-CORE=${1:?usage: asic/orfs/run.sh <core> [platform] [period ns]}
+CONFIG=${1:?usage: asic/orfs/run.sh <config> [platform] [period ns]}
 PLATFORM=${2:-sky130hd}
 PERIOD=${3:-8.0}
 IMAGE=${ORFS_IMAGE:-openroad/orfs@sha256:8b4f3942318d740ea1f73f4f895bbac150b32e41eb3b7baf7722adec6538bbcf}
 
-WORK=$REPO/build/orfs/$PLATFORM/${CORE}_${PERIOD}ns
+WORK=$REPO/build/orfs/$PLATFORM/${CONFIG}_${PERIOD}ns
 mkdir -p "$WORK/src"
 
 # 1. one plain Verilog file
-SRC=$("$REPO/tools/core_sources.sh" "$CORE" "$WORK/src/patched")
+SRC=$("$REPO/tools/core_sources.sh" "$CONFIG" "$WORK/src/patched")
 yosys -q -l "$WORK/src/frontend.log" -p "read_slang $SRC --top rabbit_cpu -DSYNTHESIS; \
           hierarchy -top rabbit_cpu; proc; opt_clean; bmuxmap; bwmuxmap; demuxmap; \
-          write_verilog -noattr $WORK/src/$CORE.v"
+          write_verilog -noattr $WORK/src/$CONFIG.v"
 
 # 2. ORFS design configuration
 cat > "$WORK/config.mk" <<EOF
 export PLATFORM        = $PLATFORM
 export DESIGN_NAME     = rabbit_cpu
-export DESIGN_NICKNAME = $CORE
-export VERILOG_FILES   = $WORK/src/$CORE.v
+export DESIGN_NICKNAME = $CONFIG
+export VERILOG_FILES   = $WORK/src/$CONFIG.v
 export SDC_FILE        = $REPO/asic/orfs/constraint.sdc
 export CLOCK_PERIOD    = $PERIOD
 # moderate density: the same for every core
@@ -45,7 +47,7 @@ EOF
 docker run --rm -u "$(id -u):$(id -g)" -v "$REPO:$REPO" -e CLOCK_PERIOD="$PERIOD" "$IMAGE" bash -c "
   cd /OpenROAD-flow-scripts && source env.sh > /dev/null 2>&1
   make -C flow DESIGN_CONFIG=$WORK/config.mk WORK_HOME=$WORK
-" > "$WORK/flow.log" 2>&1 || { echo "$CORE: flow failed, see $WORK/flow.log"; tail -20 "$WORK/flow.log"; exit 1; }
+" > "$WORK/flow.log" 2>&1 || { echo "$CONFIG: flow failed, see $WORK/flow.log"; tail -20 "$WORK/flow.log"; exit 1; }
 
 # 3. summary
-"$REPO/asic/orfs/summary.py" "$WORK" "$CORE" "$PERIOD" "$PLATFORM"
+"$REPO/asic/orfs/summary.py" "$WORK" "$CONFIG" "$PERIOD" "$PLATFORM"
diff --git a/configs/README.md b/configs/README.md
new file mode 100644
index 0000000..553dd78
--- /dev/null
+++ b/configs/README.md
@@ -0,0 +1,47 @@
+# SoC configurations
+
+One file per SoC variant. A file names the core and lists the options that
+differ from the defaults (the defaults are the full current specification,
+see `mk/config.mk`).
+
+```make
+# configs/rabbit5_rv32i.mk
+CONFIG_CORE := rabbit5
+RV32M := 0
+```
+
+Every command takes `CONFIG=<file name>`; `CORE=<core>` is the short form for
+the core's default configuration (`configs/<core>.mk`):
+
+```sh
+make soc-sim CONFIG=rabbit5_rv32i PROG=muldiv
+make formal  CONFIG=rabbit5_rv32i
+tools/synth_sky130.sh rabbit5 rabbit5_rv32i
+asic/orfs/run.sh rabbit5_rv32i
+```
+
+Build folders are named after the configuration (`build/gls/<CONFIG>`,
+`sw/baremetal/build/<CONFIG>`, ...), so variants never mix.
+
+| Configuration | Core | Options | ISA |
+|---|---|---|---|
+| `rabbit3` | rabbit3 | defaults | RV32IM + Zicsr |
+| `rabbit3_rv32i` | rabbit3 | `RV32M := 0` | RV32I + Zicsr |
+| `rabbit5` | rabbit5 | defaults | RV32IM + Zicsr |
+| `rabbit5_rv32i` | rabbit5 | `RV32M := 0` | RV32I + Zicsr |
+| `cv32e40p`, `cve2`, `ibex` | reference cores | fixed | RV32IMC + Zicsr |
+
+## Options
+
+| Option | Default | Meaning | Where it acts |
+|---|---|---|---|
+| `RV32M` | 1 | M extension: MUL, MULH*, DIV*, REM* | `rabbit_decoder` (illegal if 0), `rabbit_execute` (no `rabbit_muldiv` if 0), `misa`, `-march`, riscv-formal ISA |
+
+Rules:
+- options are set only in these files, never on the command line, so a
+  build folder always matches its name;
+- a reference core accepts only the defaults (its `core.mk` stops the build
+  otherwise);
+- every option has a test that the hardware really is absent when it is off
+  (for `RV32M := 0`: riscv-formal's `ill` check with ISA `rv32i`, and
+  `PROG=muldiv`, which then checks that every M instruction traps).
diff --git a/configs/cv32e40p.mk b/configs/cv32e40p.mk
new file mode 100644
index 0000000..94abb3a
--- /dev/null
+++ b/configs/cv32e40p.mk
@@ -0,0 +1,3 @@
+# cv32e40p: reference core (third_party/), in its fixed configuration: RV32IMC + Zicsr.
+# Its options are not switchable here (rtl/cores/cv32e40p/core.mk).
+CONFIG_CORE := cv32e40p
diff --git a/configs/cve2.mk b/configs/cve2.mk
new file mode 100644
index 0000000..4c5803a
--- /dev/null
+++ b/configs/cve2.mk
@@ -0,0 +1,3 @@
+# cve2: reference core (third_party/), in its fixed configuration: RV32IMC + Zicsr.
+# Its options are not switchable here (rtl/cores/cve2/core.mk).
+CONFIG_CORE := cve2
diff --git a/configs/ibex.mk b/configs/ibex.mk
new file mode 100644
index 0000000..5ffd3ce
--- /dev/null
+++ b/configs/ibex.mk
@@ -0,0 +1,3 @@
+# ibex: reference core (third_party/), in its fixed configuration: RV32IMC + Zicsr.
+# Its options are not switchable here (rtl/cores/ibex/core.mk).
+CONFIG_CORE := ibex
diff --git a/configs/rabbit3.mk b/configs/rabbit3.mk
new file mode 100644
index 0000000..803e852
--- /dev/null
+++ b/configs/rabbit3.mk
@@ -0,0 +1,2 @@
+# rabbit3: our 3-stage core, full specification (RV32IM + Zicsr)
+CONFIG_CORE := rabbit3
diff --git a/configs/rabbit3_rv32i.mk b/configs/rabbit3_rv32i.mk
new file mode 100644
index 0000000..04f90e2
--- /dev/null
+++ b/configs/rabbit3_rv32i.mk
@@ -0,0 +1,4 @@
+# rabbit3 without the M extension: smallest rabbit3. MUL/DIV/REM trap as
+# illegal instructions; the compiler uses software multiply/divide instead.
+CONFIG_CORE := rabbit3
+RV32M := 0
diff --git a/configs/rabbit5.mk b/configs/rabbit5.mk
new file mode 100644
index 0000000..c47566e
--- /dev/null
+++ b/configs/rabbit5.mk
@@ -0,0 +1,2 @@
+# rabbit5: our 5-stage core, full specification (RV32IM + Zicsr)
+CONFIG_CORE := rabbit5
diff --git a/configs/rabbit5_rv32i.mk b/configs/rabbit5_rv32i.mk
new file mode 100644
index 0000000..876d8cc
--- /dev/null
+++ b/configs/rabbit5_rv32i.mk
@@ -0,0 +1,4 @@
+# rabbit5 without the M extension. MUL/DIV/REM trap as illegal instructions;
+# the compiler uses software multiply/divide instead.
+CONFIG_CORE := rabbit5
+RV32M := 0
diff --git a/docs/GETTING_STARTED.md b/docs/GETTING_STARTED.md
index 1e23e3f..a2c24e7 100644
--- a/docs/GETTING_STARTED.md
+++ b/docs/GETTING_STARTED.md
@@ -32,7 +32,7 @@ make ci          # lint + SoC firmware sim + 10 hw_ip tests + rma_analysis examp
 | 7 | `dv/cocotb/soc/test_soc.py` | Testbench: clock, reset, console capture, pass/fail |
 
 ```bash
-make soc-sim                 # CORE=cv32e40p PROG=hello by default
+make soc-sim                 # CONFIG=cv32e40p PROG=hello by default (configs/)
 make soc-waves               # same, plus dv/cocotb/soc/dump.fst
 gtkwave dv/cocotb/soc/dump.fst   # or: surfer dump.fst
 ```
diff --git a/docs/STATUS.md b/docs/STATUS.md
index cf02b08..1995eac 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -12,6 +12,7 @@
 | Interrupt self-test on CV32E40P (reference) | `make soc-sim PROG=irq` | PASS, 9095 cycles |
 | Reference cores CVE2 and Ibex (pinned submodules, same firmware) | `make soc-sim CORE=cve2\|ibex PROG=...` | hello / irq / muldiv PASS; comparison table in `rtl/cores/README.md` |
 | Reproduce everything | `tools/check_all.sh [quick gls formal synth mutants]` | all PASS (2026-11-07) |
+| SoC configurations (`configs/`, `make configs`): core + options, one name per variant | `make <target> CONFIG=rabbit5_rv32i` | 7 configurations; quick, gls, formal all PASS (2026-11-07) |
 
 ## Own cores: rabbit3 and rabbit5 (shared blocks in rtl/cores/rabbit_common)
 
@@ -27,6 +28,9 @@
 | interrupt properties I1–I4, sleep W0–W2; worst-case latency (tight) | PASS, 4 cycles | PASS, 7 cycles |
 | gate-level smoke (`make gls-smoke CORE=...`) | PASS, same cycles (hello, irq, muldiv) | PASS, same cycles (hello, irq, muldiv) |
 | size, sky130 (`synth -booth` + ABC; CV32E40P RV32IMC: 170.3 k µm²) | 114.9 k µm² | 126.5 k µm² |
+| without M (`CONFIG=rabbit3_rv32i` / `rabbit5_rv32i`): size | 81.1 k µm² (−29 %) | 95.2 k µm² (−25 %) |
+| without M: riscv-formal / timing + X1 (MUL/DIV trap) / gate level | 45/45 / PASS / PASS | 45/45 / PASS / PASS |
+| without M: hello / muldiv (software multiply via libgcc) | 3147 / 62 724 cycles | 3960 / 75 013 cycles |
 
 Next: int8 (and int4) SIMD dot product for quantized inference, riscv-formal
 CSR checks, RISCOF compliance, then the dual-core TDM work (M4).
diff --git a/dv/cocotb/soc/Makefile b/dv/cocotb/soc/Makefile
index c7f1182..4d9a783 100644
--- a/dv/cocotb/soc/Makefile
+++ b/dv/cocotb/soc/Makefile
@@ -1,14 +1,14 @@
-# cocotb + Verilator: run a firmware image on rabbit_soc_sim with the selected core.
-#   uv run make                      # core=cv32e40p, prog=hello
-#   uv run make PROG=hello WAVES=1   # also dump dump.fst for GTKWave/Surfer
+# cocotb + Verilator: run a firmware image on rabbit_soc_sim, one SoC configuration.
+#   uv run make                              # CONFIG=cv32e40p, PROG=hello
+#   uv run make CONFIG=rabbit5_rv32i PROG=muldiv
+#   uv run make PROG=hello WAVES=1           # also dump dump.fst for GTKWave/Surfer
 REPO ?= $(abspath ../../..)
 export REPO
-CORE ?= cv32e40p
 PROG ?= hello
 
-include $(REPO)/rtl/cores/$(CORE)/core.mk
+include $(REPO)/mk/config.mk
 
-FIRMWARE := $(REPO)/sw/baremetal/build/$(CORE)/$(PROG)/$(PROG).hex
+FIRMWARE := $(REPO)/sw/baremetal/build/$(CONFIG)/$(PROG)/$(PROG).hex
 export RABBIT_FIRMWARE := $(FIRMWARE)
 export RABBIT_PROG := $(PROG)
 
@@ -16,17 +16,17 @@ SIM            ?= verilator
 TOPLEVEL_LANG   = verilog
 TOPLEVEL        = rabbit_soc_sim
 COCOTB_TEST_MODULES = test_soc
-SIM_BUILD      ?= sim_build_$(CORE)
+SIM_BUILD      ?= sim_build_$(CONFIG)
 
 # Sources come from the per-core and SoC file lists (${REPO} is expanded by Verilator).
 # GLS=1 replaces the core RTL by its gate-level netlist (see `make gls-netlist`).
 VERILOG_SOURCES =
 ifeq ($(GLS),1)
-NETLIST    ?= $(REPO)/build/gls/$(CORE)/rabbit_cpu_netlist.v
+NETLIST    ?= $(REPO)/build/gls/$(CONFIG)/rabbit_cpu_netlist.v
 EXTRA_ARGS += $(NETLIST) -Wno-fatal -DRABBIT_GLS
-SIM_BUILD   = sim_build_$(CORE)_gls
+SIM_BUILD   = sim_build_$(CONFIG)_gls
 else
-EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f $(CORE_VERILATOR_FLAGS)
+EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f $(CORE_VERILATOR_FLAGS) $(CONFIG_DEFINES)
 endif
 EXTRA_ARGS += -f $(REPO)/rtl/soc/files.f -DRABBIT_QUIET
 ifeq ($(WAVES),1)
@@ -34,7 +34,7 @@ ifeq ($(WAVES),1)
 # (a traced model is slower, so the normal build stays trace-free).
 EXTRA_ARGS += --trace-fst --trace-structs
 SIM_ARGS   += --trace
-SIM_BUILD   = sim_build_$(CORE)_waves
+SIM_BUILD   = sim_build_$(CONFIG)_waves
 endif
 # extra Verilator options, e.g. --trace-underscore for the energy flow (asic/orfs/energy.sh)
 EXTRA_ARGS += $(VERILATOR_EXTRA)
@@ -47,7 +47,7 @@ CUSTOM_COMPILE_DEPS += $(call expand_f,$(REPO)/rtl/soc/files.f)
 ifeq ($(GLS),1)
 CUSTOM_COMPILE_DEPS += $(NETLIST)
 else
-CUSTOM_COMPILE_DEPS += $(filter %.sv %.v,$(call expand_f,$(REPO)/rtl/cores/$(CORE)/files.f))
+CUSTOM_COMPILE_DEPS += $(filter %.sv %.v,$(call expand_f,$(REPO)/rtl/cores/$(CORE)/files.f)) $(CONFIG_DEPS)
 endif
 
 COCOTB_HDL_TIMEUNIT      = 1ns
@@ -58,5 +58,5 @@ include $(shell cocotb-config --makefiles)/Makefile.sim
 # Always rebuild the firmware before simulating.
 sim: firmware
 firmware:
-	$(MAKE) -C $(REPO)/sw/baremetal PROG=$(PROG) CORE=$(CORE)
+	$(MAKE) -C $(REPO)/sw/baremetal PROG=$(PROG) CONFIG=$(CONFIG)
 .PHONY: firmware
diff --git a/dv/formal/README.md b/dv/formal/README.md
index 4ee06fb..6d1bffd 100644
--- a/dv/formal/README.md
+++ b/dv/formal/README.md
@@ -2,10 +2,12 @@
 
 ## rabbit cores (rabbit3, rabbit5)
 
-One flow for every rabbit core, selected with `CORE=`:
+One flow for every rabbit configuration (`configs/`), selected with
+`CONFIG=` (`CORE=rabbit3` is short for `CONFIG=rabbit3`):
 
 ```bash
 make formal CORE=rabbit3                       # from the repo root: everything below
+make formal CONFIG=rabbit3_rv32i               # the same core without M (proves MUL/DIV trap: X1)
 make -C dv/formal/rabbit CORE=rabbit5 riscv-formal
 make -C dv/formal/rabbit CORE=rabbit5 timing
 make -C dv/formal/rabbit muldiv                               # multiply/divide unit (any core)
diff --git a/dv/formal/rabbit/Makefile b/dv/formal/rabbit/Makefile
index 4047214..b91f884 100644
--- a/dv/formal/rabbit/Makefile
+++ b/dv/formal/rabbit/Makefile
@@ -1,4 +1,5 @@
-# Formal verification of a rabbit core:  make CORE=rabbit3   (default rabbit5)
+# Formal verification of a rabbit configuration (configs/):
+#   make CONFIG=rabbit3_rv32i   (default rabbit5; CORE=rabbit3 = CONFIG=rabbit3)
 #   make                 riscv-formal checks + timing properties + muldiv
 #   make riscv-formal    only riscv-formal (parallel)
 #   make timing          only the timing properties (timing/rabbit_timing_tb.sv)
@@ -6,16 +7,20 @@
 #   make muldiv-sim      ... its exhaustive 8-bit simulation part
 #   make check C=insn_add_ch0   one riscv-formal check
 REPO   ?= $(abspath ../../..)
-CORE   ?= rabbit5
+CONFIG ?= $(if $(CORE),$(CORE),rabbit5)
 JOBS   ?= $(shell nproc)
 RF_SRC := $(REPO)/third_party/riscv-formal
 
-include $(REPO)/rtl/cores/$(CORE)/core.mk
+include $(REPO)/mk/config.mk
+ifeq ($(filter rabbit%,$(CORE)),)
+$(error formal: CONFIG=$(CONFIG) uses $(CORE); these proofs are for the rabbit cores)
+endif
+HAS_M := $(filter 1,$(RV32M))
 
 # 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)
+BUILD    := build/$(CONFIG)
 FLAT     := $(BUILD)/core_flat.v
 # genchecks.py expects <riscv-formal>/cores/<core>/, so build a small mirror
 MIRROR   := $(BUILD)/riscv-formal
@@ -37,14 +42,14 @@ generate: $(CORE_DIR)/checks/makefile
 # built-in parser, so convert once with the slang frontend.
 # M extension: riscv-formal checks MUL/DIV with stand-in results (ALTOPS) and
 # a short divider (FORMAL_DIV_STEPS); the real arithmetic is the muldiv proof.
-FORMAL_DEFINES := -DSYNTHESIS -DRISCV_FORMAL_ALTOPS -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS)
-$(FLAT): $(SOURCES) $(REPO)/rtl/cores/$(CORE)/core.mk
+FORMAL_DEFINES := -DSYNTHESIS -DRISCV_FORMAL_ALTOPS -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS) $(CONFIG_DEFINES)
+$(FLAT): $(SOURCES) $(CONFIG_DEPS)
 	@mkdir -p $(BUILD)
 	yosys $(YOSYS_SLANG) -q -p "read_slang $(SOURCES) --top $(CORE)_core $(FORMAL_DEFINES); \
 	             hierarchy -top $(CORE)_core; proc; flatten; opt_clean; \
 	             write_verilog -noattr $@"
 
-$(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv $(REPO)/rtl/cores/$(CORE)/core.mk
+$(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv $(CONFIG_DEPS)
 	@mkdir -p $(MIRROR) $(CORE_DIR)
 	ln -sfn $(RF_SRC)/checks $(MIRROR)/checks
 	ln -sfn $(RF_SRC)/insns  $(MIRROR)/insns
@@ -52,6 +57,8 @@ $(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv $(REPO)/rtl/cores/$(C
 	sed -e 's/@RABBIT_CORE@/$(CORE)_core/' \
 	    -e 's/@LIVENESS_DEPTH@/$(FORMAL_LIVENESS_DEPTH)/' \
 	    -e 's/@RABBIT_IRQ_DEFINE@/$(if $(filter-out 0,$(TIMING_IRQ_LATENCY)),`define RABBIT_HAS_IRQ)/' \
+	    -e 's/@RABBIT_M_DEFINE@/$(if $(HAS_M),`define RABBIT_HAS_M)/' \
+	    -e 's/@ISA@/$(CONFIG_ISA)/' \
 	    checks.cfg > $(CORE_DIR)/checks.cfg
 	rm -rf $(CORE_DIR)/checks
 	cd $(CORE_DIR) && python3 ../../checks/genchecks.py
@@ -70,12 +77,13 @@ TIMING_DEFINES := -DSYNTHESIS -DRISCV_FORMAL_ALTOPS -DRABBIT_CORE=$(CORE)_core \
                   -DIRQ_LATENCY=$(TIMING_IRQ_LATENCY) \
                   -DCOMMIT_TO_RETIRE=$(TIMING_COMMIT_TO_RETIRE) \
                   -DMUL_CYCLES=$(TIMING_MUL_CYCLES) \
-                  -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS)
+                  -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS) \
+                  $(CONFIG_DEFINES) $(if $(HAS_M),-DRABBIT_HAS_M)
 
 timing: $(BUILD)/timing.sby
 	cd $(BUILD) && sby -f timing.sby
 
-$(BUILD)/timing.sby: timing/timing.sby.in timing/rabbit_timing_tb.sv $(SOURCES) $(REPO)/rtl/cores/$(CORE)/core.mk
+$(BUILD)/timing.sby: timing/timing.sby.in timing/rabbit_timing_tb.sv $(SOURCES) $(CONFIG_DEPS)
 	@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
diff --git a/dv/formal/rabbit/checks.cfg b/dv/formal/rabbit/checks.cfg
index 32676f0..b9f6c66 100644
--- a/dv/formal/rabbit/checks.cfg
+++ b/dv/formal/rabbit/checks.cfg
@@ -1,5 +1,5 @@
 # riscv-formal configuration TEMPLATE for the rabbit cores (see dv/formal/README.md).
-# The Makefile fills in @RABBIT_CORE@ for CORE=rabbit3|rabbit5.
+# The Makefile fills in the @...@ fields from the configuration (configs/, core.mk).
 #
 # [depth] columns: <check>  [start]  [step to check at]   (BMC cycles)
 # The first instruction retires 3 (rabbit3) or 5 (rabbit5) cycles after reset.
@@ -11,7 +11,7 @@
 # ~3 + 7 + 3 cycles away on rabbit5. Per core: FORMAL_LIVENESS_DEPTH (core.mk).
 
 [options]
-isa rv32im
+isa @ISA@
 
 [depth]
 insn            12
@@ -32,6 +32,7 @@ reg_ch0
 `define RISCV_FORMAL_ALTOPS
 `define RABBIT_CORE @RABBIT_CORE@
 @RABBIT_IRQ_DEFINE@
+@RABBIT_M_DEFINE@
 
 [verilog-files]
 @basedir@/cores/@core@/wrapper.sv
@@ -44,7 +45,9 @@ reg_ch0
 # (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);
+`ifdef RABBIT_HAS_M
 always @* if (!reset) cover (channel[0].valid && channel[0].insn[6:0] == 7'b0110011 && channel[0].insn[31:25] == 7'b0000001 && channel[0].insn[14]);
+`endif
 `ifdef RABBIT_HAS_IRQ
 always @* if (!reset) cover (channel[0].valid && channel[0].intr);
 `endif
diff --git a/dv/formal/rabbit/timing/rabbit_timing_tb.sv b/dv/formal/rabbit/timing/rabbit_timing_tb.sv
index 4feba28..e872514 100644
--- a/dv/formal/rabbit/timing/rabbit_timing_tb.sv
+++ b/dv/formal/rabbit/timing/rabbit_timing_tb.sv
@@ -18,6 +18,7 @@
 //   RABBIT_DIV_STEPS  divider steps in this proof; a DIV* spends
 //                  RABBIT_DIV_STEPS+2 cycles in the commit stage (see core.mk:
 //                  the proof uses 2 steps, the real 32 are proven in muldiv/)
+//   RABBIT_HAS_M   defined if the configuration has the M extension (RV32M = 1)
 //
 //   T1  exact timing model: the gap between two consecutive retirements is
 //         REDIRECT_GAP  if the earlier instruction changed control flow
@@ -50,7 +51,7 @@
 //       vector the core jumped to)
 //   I5  the handler starts at the right address: mtvec base (direct mode) or
 //       base + 4*line for a requested line (vectored mode)
-// M extension:
+// M extension (the covers of M1 and R8 only if RABBIT_HAS_M):
 //   M0  while an M instruction waits in the commit stage, its operand values
 //       do not change (rabbit_muldiv relies on it; white-box: looks inside
 //       rabbit_execute)
@@ -59,6 +60,8 @@
 //       it happens)
 //   M2  while an M instruction waits, no instruction is fetched (power: a
 //       divide costs no instruction-memory reads)
+//   X1  without the M extension: every MUL/DIV/REM encoding traps (illegal
+//       instruction) and writes nothing: the hardware is really absent
 // Sleep (WFI), for power:
 //   W0  the core only falls asleep when a WFI retires
 //   W1  it wakes in the cycle after an enabled interrupt becomes pending
@@ -175,6 +178,17 @@ module rabbit_timing_tb (
   assign is_m    = (opcode == 7'b0110011) && (rvfi_insn[31:25] == 7'b0000001) && !rvfi_trap;
   assign m_extra = !is_m ? 0 : funct3[2] ? DIV_CYCLES - 1 : MUL_CYCLES - 1;
 
+`ifndef RABBIT_HAS_M
+  // X1: without M, the M encodings are illegal instructions
+  logic m_encoding;
+  assign m_encoding = (opcode == 7'b0110011) && (rvfi_insn[31:25] == 7'b0000001);
+  always_comb begin
+    if (rst_n && rvfi_valid && m_encoding)
+      assert (rvfi_trap && rvfi_rd_addr == 5'd0 && rvfi_mem_wmask == 4'd0);   // X1
+    if (rst_n && rvfi_valid && m_encoding) cover (!rvfi_intr);              // X1 happens
+  end
+`endif
+
   // CSR instructions (the ISA meaning: old value -> rd, then write)
   logic        is_csr, csr_writes;
   logic [11:0] csr_addr;
@@ -421,7 +435,9 @@ module rabbit_timing_tb (
         cover (wait_cycles + D == IRQ_LATENCY && m_extra == 0);   // the bound is tight
         cover (wait_cycles + D == IRQ_LATENCY - 1);
         cover (slept);                            // WFI woken by the interrupt it takes
+`ifdef RABBIT_HAS_M
         cover (m_busy_seen);                      // M1: interrupt while an M op waited
+`endif
         cover (!m_tvec[0]);                       // direct mode is exercised too
         cover (m_tvec[0] && vec_line != 7);       // ... and a vector other than the timer's
       end
@@ -460,9 +476,11 @@ module rabbit_timing_tb (
       cover (gap == LOADUSE_GAP && load_use);
       cover (gap == REDIRECT_GAP);
       cover (gap == REDIRECT_GAP && rvfi_trap);
+`ifdef RABBIT_HAS_M
       cover (is_m && !funct3[2] && gap == MUL_CYCLES);       // R8: multiply
       cover (is_m &&  funct3[2] && gap == DIV_CYCLES);       // R8: divide
       cover (is_m && load_use);                              // R8 after load-use
+`endif
     end
   end
 endmodule
diff --git a/mk/config.mk b/mk/config.mk
new file mode 100644
index 0000000..c14fa5b
--- /dev/null
+++ b/mk/config.mk
@@ -0,0 +1,63 @@
+# =============================================================================
+# mk/config.mk — turn a configuration name into everything a build needs
+# =============================================================================
+# Included by every Makefile that builds, simulates, proves or synthesizes a
+# SoC. A configuration is one small file, configs/<CONFIG>.mk: which core, and
+# which optional parts are switched on (see configs/README.md).
+#
+#   make soc-sim CONFIG=rabbit5_rv32i    any file in configs/
+#   make soc-sim CORE=rabbit5            short form: CONFIG=rabbit5, the core's
+#                                        default configuration
+#
+# After this file:
+#   CONFIG          name, also the name of every build folder
+#   CORE            rtl/cores/<CORE>/ (rabbit_cpu.sv, files.f, core.mk)
+#   RV32M           1/0, and the other options below
+#   CONFIG_DEFINES  the options as -D defines, for every tool that reads RTL
+#                   (Verilator, Yosys/slang, SymbiYosys). They become the CFG
+#                   parameter of the rabbit cores (rtl/cores/rabbit_common/rabbit_pkg.sv).
+#   CONFIG_ISA      ISA string without Zicsr, e.g. rv32im (riscv-formal, -march)
+#   + everything rtl/cores/<CORE>/core.mk sets (CORE_MARCH, TIMING_*, ...)
+# =============================================================================
+REPO ?= $(abspath $(dir $(lastword $(MAKEFILE_LIST)))/..)
+
+CONFIG ?= $(if $(CORE),$(CORE),cv32e40p)
+CONFIG_FILE := $(REPO)/configs/$(CONFIG).mk
+ifeq ($(wildcard $(CONFIG_FILE)),)
+$(error CONFIG=$(CONFIG): there is no configs/$(CONFIG).mk. Available: $(sort $(basename $(notdir $(wildcard $(REPO)/configs/*.mk)))))
+endif
+
+# ---- options and their defaults --------------------------------------------
+# The defaults are the full current specification; a configuration file only
+# lists what differs. Options are set in configuration files, never on the
+# command line: every build folder is named after CONFIG, so two builds with
+# the same name must be the same hardware.
+CONFIG_OPTIONS := RV32M
+# RV32M: M extension (multiply / divide)
+RV32M := 1
+
+$(foreach o,$(CONFIG_OPTIONS),$(if $(filter command line environment,$(origin $(o))),\
+  $(error $(o) is an option of a configuration: set it in configs/$(CONFIG).mk (or a new file there), not on the command line)))
+
+include $(CONFIG_FILE)
+ifeq ($(CONFIG_CORE),)
+$(error configs/$(CONFIG).mk must set CONFIG_CORE)
+endif
+ifneq ($(filter command line environment,$(origin CORE)),)
+ifneq ($(CORE),$(CONFIG_CORE))
+$(error CORE=$(CORE) but configs/$(CONFIG).mk uses core $(CONFIG_CORE); give only CONFIG)
+endif
+endif
+override CORE := $(CONFIG_CORE)
+
+# strip: a comment after a value ("RV32M := 0  # ...") leaves trailing spaces
+RV32M := $(strip $(RV32M))
+$(if $(filter-out 0 1,$(RV32M)),$(error configs/$(CONFIG).mk: RV32M must be 0 or 1))
+
+CONFIG_ISA     := rv32i$(if $(filter 1,$(RV32M)),m)
+CONFIG_DEFINES := -DRABBIT_RV32M=$(RV32M)
+
+include $(REPO)/rtl/cores/$(CORE)/core.mk
+
+# A build depends on its configuration: editing it rebuilds what used it.
+CONFIG_DEPS := $(CONFIG_FILE) $(REPO)/mk/config.mk $(REPO)/rtl/cores/$(CORE)/core.mk
diff --git a/rtl/cores/README.md b/rtl/cores/README.md
index 5419e46..d242a65 100644
--- a/rtl/cores/README.md
+++ b/rtl/cores/README.md
@@ -10,7 +10,8 @@ support lives in its own sub-directory and provides:
 | `files.f` | Verilator/Yosys file list (paths relative to the repo root via the `${REPO}` environment variable) |
 | `core.mk` | Make fragment: `CORE_MARCH`, `CORE_MABI`, extra simulator flags; `CORE_CFLAGS` for documented deviations from the contract (seen by the firmware) |
 
-Select a core with `make CORE=<dir-name> ...` (default: `cv32e40p`).
+Select a core with `make CORE=<dir-name> ...` (default: `cv32e40p`), or a
+variant of it with `make CONFIG=<name> ...` (`configs/README.md`).
 Only one `rabbit_cpu` is compiled per build, so no `ifdef` soup is needed.
 
 ## Port contract (v0)
diff --git a/rtl/cores/cv32e40p/core.mk b/rtl/cores/cv32e40p/core.mk
index 7cb339d..e7dffb9 100644
--- a/rtl/cores/cv32e40p/core.mk
+++ b/rtl/cores/cv32e40p/core.mk
@@ -1,4 +1,9 @@
-# Per-core build settings, included by the top-level and dv Makefiles.
+# Per-core build settings, included by mk/config.mk after the configuration.
+# Reference core in a fixed configuration: only the default options.
+ifneq ($(RV32M),1)
+$(error $(CORE) is a reference core in a fixed configuration (RV32IMC); RV32M cannot be 0)
+endif
+CONFIG_ISA       := rv32imc
 CORE_MARCH       := rv32imc_zicsr
 CORE_MABI        := ilp32
 # Vendor code: keep warnings non-fatal. COMBDLY: bhv/cv32e40p_sim_clock_gate.sv
diff --git a/rtl/cores/cve2/core.mk b/rtl/cores/cve2/core.mk
index 732f7cf..3476dc7 100644
--- a/rtl/cores/cve2/core.mk
+++ b/rtl/cores/cve2/core.mk
@@ -1,4 +1,9 @@
-# Per-core build settings, included by the top-level and dv Makefiles.
+# Per-core build settings, included by mk/config.mk after the configuration.
+# Reference core in a fixed configuration: only the default options.
+ifneq ($(RV32M),1)
+$(error $(CORE) is a reference core in a fixed configuration (RV32IMC); RV32M cannot be 0)
+endif
+CONFIG_ISA       := rv32imc
 CORE_MARCH       := rv32imc_zicsr
 CORE_MABI        := ilp32
 # Vendor code: keep warnings non-fatal.
diff --git a/rtl/cores/ibex/core.mk b/rtl/cores/ibex/core.mk
index f0168a9..9e3f3ce 100644
--- a/rtl/cores/ibex/core.mk
+++ b/rtl/cores/ibex/core.mk
@@ -1,4 +1,9 @@
-# Per-core build settings, included by the top-level and dv Makefiles.
+# Per-core build settings, included by mk/config.mk after the configuration.
+# Reference core in a fixed configuration: only the default options.
+ifneq ($(RV32M),1)
+$(error $(CORE) is a reference core in a fixed configuration (RV32IMC); RV32M cannot be 0)
+endif
+CONFIG_ISA       := rv32imc
 CORE_MARCH       := rv32imc_zicsr
 CORE_MABI        := ilp32
 # Vendor code: keep warnings non-fatal; Ibex' own Verilator waivers are not used.
diff --git a/rtl/cores/rabbit3/core.mk b/rtl/cores/rabbit3/core.mk
index d74bde7..7689c3c 100644
--- a/rtl/cores/rabbit3/core.mk
+++ b/rtl/cores/rabbit3/core.mk
@@ -1,5 +1,6 @@
-# Per-core build settings, included by the top-level and dv Makefiles.
-CORE_MARCH       := rv32im_zicsr
+# Per-core build settings, included by mk/config.mk after the configuration
+# (configs/<CONFIG>.mk): CONFIG_ISA and the options are already known here.
+CORE_MARCH       := $(CONFIG_ISA)_zicsr
 CORE_MABI        := ilp32
 # Our own RTL: no warning suppressions.
 CORE_VERILATOR_FLAGS :=
@@ -15,7 +16,7 @@ TIMING_IRQ_LATENCY  := 4
 # Cycles from the commit stage (X) to retirement (W). The timing testbench
 # uses it to line up its RVFI-based spec model with the core.
 TIMING_COMMIT_TO_RETIRE := 1
-# M extension (rule R8): cycles an instruction spends in X, for any
+# M extension (rule R8, only with RV32M = 1): cycles an instruction spends in X, for any
 # operands. FORMAL_DIV_STEPS is the divider's step count used by the
 # pipeline-level proofs (a 34-cycle divide does not fit in their depth); the
 # real 32 steps are proven in dv/formal/rabbit/muldiv (L1).
@@ -25,4 +26,5 @@ FORMAL_DIV_STEPS    := 2
 # riscv-formal liveness: the check cycle (window = depth - 8). An interrupted
 # divide plus a handler that starts with a divide needs a long window;
 # measured: 16 fails (a real longer gap), 18 passes.
-FORMAL_LIVENESS_DEPTH := 20
+# Without M the window of the original RV32I proof (15) is enough.
+FORMAL_LIVENESS_DEPTH := $(if $(filter 1,$(RV32M)),20,15)
diff --git a/rtl/cores/rabbit3/rabbit3_core.sv b/rtl/cores/rabbit3/rabbit3_core.sv
index 2386786..497d0a4 100644
--- a/rtl/cores/rabbit3/rabbit3_core.sv
+++ b/rtl/cores/rabbit3/rabbit3_core.sv
@@ -1,5 +1,5 @@
 // =============================================================================
-// rabbit3_core — 3-stage in-order RV32IM pipeline (single hart)
+// rabbit3_core — 3-stage in-order RV32I(M) pipeline (single hart)
 // =============================================================================
 // START HERE to learn the rabbit pipelines; then read rabbit5_core.sv.
 //
@@ -59,6 +59,7 @@
 module rabbit3_core
   import rabbit_pkg::*;
 #(
+  parameter rabbit_cfg_t CFG        = RABBIT_CFG,     // optional ISA parts (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
@@ -177,7 +178,7 @@ module rabbit3_core
   end
 
   decoded_t x_dec;
-  rabbit_decoder u_decoder (.instr_i(x_instr), .dec_o(x_dec));
+  rabbit_decoder #(.CFG(CFG)) u_decoder (.instr_i(x_instr), .dec_o(x_dec));
 
   // Register file: read in X, written in W. The write-first bypass inside
   // is this core's entire forwarding network. While X is held (R8), the
@@ -192,7 +193,7 @@ module rabbit3_core
   );
 
   exec_t x_res;
-  rabbit_execute #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute (
+  rabbit_execute #(.CFG(CFG), .MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute (
     .clk_i, .rst_ni,
     .valid_i      (x_valid_q),
     .pc_i         (x_pc_q),
diff --git a/rtl/cores/rabbit3/rabbit_cpu.sv b/rtl/cores/rabbit3/rabbit_cpu.sv
index 28f10da..7d6f759 100644
--- a/rtl/cores/rabbit3/rabbit_cpu.sv
+++ b/rtl/cores/rabbit3/rabbit_cpu.sv
@@ -1,7 +1,9 @@
-// rabbit_cpu adapter for rabbit3 (our own 3-stage RV32IM core).
+// rabbit_cpu adapter for rabbit3 (our own 3-stage RV32I core, M optional).
 // 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 #(
+    // optional ISA parts; the default comes from the build (configs/, rabbit_pkg)
+    parameter rabbit_pkg::rabbit_cfg_t CFG = rabbit_pkg::RABBIT_CFG,
     parameter logic [31:0] BOOT_ADDR  = 32'h0000_0080,
     parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000
 ) (
@@ -31,7 +33,7 @@ module rabbit_cpu #(
     input  logic        debug_req_i,
     output logic        core_sleep_o
 );
-  rabbit3_core #(.BOOT_ADDR(BOOT_ADDR), .MTVEC_ADDR(MTVEC_ADDR)) u_core (
+  rabbit3_core #(.CFG(CFG), .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,
diff --git a/rtl/cores/rabbit5/core.mk b/rtl/cores/rabbit5/core.mk
index 4ccf6ab..1747eaa 100644
--- a/rtl/cores/rabbit5/core.mk
+++ b/rtl/cores/rabbit5/core.mk
@@ -1,5 +1,6 @@
-# Per-core build settings, included by the top-level and dv Makefiles.
-CORE_MARCH       := rv32im_zicsr
+# Per-core build settings, included by mk/config.mk after the configuration
+# (configs/<CONFIG>.mk): CONFIG_ISA and the options are already known here.
+CORE_MARCH       := $(CONFIG_ISA)_zicsr
 CORE_MABI        := ilp32
 # Our own RTL: no warning suppressions.
 CORE_VERILATOR_FLAGS :=
@@ -15,7 +16,7 @@ TIMING_IRQ_LATENCY  := 7
 # Cycles from the commit stage (EX) to retirement (WB). The timing testbench
 # uses it to line up its RVFI-based spec model with the core.
 TIMING_COMMIT_TO_RETIRE := 2
-# M extension (rule R8): cycles an instruction spends in EX, for any
+# M extension (rule R8, only with RV32M = 1): cycles an instruction spends in EX, for any
 # operands. FORMAL_DIV_STEPS is the divider's step count used by the
 # pipeline-level proofs (a 34-cycle divide does not fit in their depth); the
 # real 32 steps are proven in dv/formal/rabbit/muldiv (L1).
@@ -25,4 +26,5 @@ FORMAL_DIV_STEPS    := 2
 # riscv-formal liveness: the check cycle (window = depth - 8). An interrupted
 # divide plus a handler that starts with a divide needs a long window;
 # measured: 26 passes in seconds; 22 does not finish in 25 min.
-FORMAL_LIVENESS_DEPTH := 26
+# Without M the window of the original RV32I proof (15) is enough.
+FORMAL_LIVENESS_DEPTH := $(if $(filter 1,$(RV32M)),26,15)
diff --git a/rtl/cores/rabbit5/rabbit5_core.sv b/rtl/cores/rabbit5/rabbit5_core.sv
index 6a43b6c..60a86a6 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 RV32IM pipeline (single hart)
+// rabbit5_core — 5-stage in-order RV32I(M) pipeline (single hart)
 // =============================================================================
 //
 //   cycle:   1    2    3    4    5    6
@@ -63,6 +63,7 @@
 module rabbit5_core
   import rabbit_pkg::*;
 #(
+  parameter rabbit_cfg_t CFG        = RABBIT_CFG,     // optional ISA parts (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
@@ -203,7 +204,7 @@ module rabbit5_core
   end
 
   decoded_t id_dec;
-  rabbit_decoder u_decoder (.instr_i(id_instr), .dec_o(id_dec));
+  rabbit_decoder #(.CFG(CFG)) u_decoder (.instr_i(id_instr), .dec_o(id_dec));
 
   // Register file: read in ID, written in WB (write-first bypass inside)
   logic [31:0] id_rs1_val, id_rs2_val;
@@ -260,7 +261,7 @@ module rabbit5_core
   assign ex_rs2 = forward(ex_q.dec.rs2, ex_q.rs2_val);
 
   exec_t ex_res;
-  rabbit_execute #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute (
+  rabbit_execute #(.CFG(CFG), .MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute (
     .clk_i, .rst_ni,
     .valid_i      (ex_q.valid),
     .pc_i         (ex_q.pc),
diff --git a/rtl/cores/rabbit5/rabbit_cpu.sv b/rtl/cores/rabbit5/rabbit_cpu.sv
index 33a8747..0d2cd4c 100644
--- a/rtl/cores/rabbit5/rabbit_cpu.sv
+++ b/rtl/cores/rabbit5/rabbit_cpu.sv
@@ -1,7 +1,9 @@
-// rabbit_cpu adapter for rabbit5 (our own 5-stage RV32IM core).
+// rabbit_cpu adapter for rabbit5 (our own 5-stage RV32I core, M optional).
 // See rtl/cores/README.md for the port contract. rabbit5 needs memories that
 // grant immediately and answer one cycle later (rabbit5_core.sv, rule R4).
 module rabbit_cpu #(
+    // optional ISA parts; the default comes from the build (configs/, rabbit_pkg)
+    parameter rabbit_pkg::rabbit_cfg_t CFG = rabbit_pkg::RABBIT_CFG,
     parameter logic [31:0] BOOT_ADDR  = 32'h0000_0080,
     parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000
 ) (
@@ -31,7 +33,7 @@ module rabbit_cpu #(
     input  logic        debug_req_i,
     output logic        core_sleep_o
 );
-  rabbit5_core #(.BOOT_ADDR(BOOT_ADDR), .MTVEC_ADDR(MTVEC_ADDR)) u_core (
+  rabbit5_core #(.CFG(CFG), .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,
diff --git a/rtl/cores/rabbit_common/rabbit_csr.sv b/rtl/cores/rabbit_common/rabbit_csr.sv
index e0d01cd..2dd1e2f 100644
--- a/rtl/cores/rabbit_common/rabbit_csr.sv
+++ b/rtl/cores/rabbit_common/rabbit_csr.sv
@@ -25,6 +25,7 @@
 module rabbit_csr
   import rabbit_pkg::*;
 #(
+  parameter rabbit_cfg_t CFG         = RABBIT_CFG,
   parameter logic [31:0] MTVEC_RESET = 32'h0,
   parameter logic [31:0] HART_ID     = 32'h0
 ) (
@@ -79,7 +80,7 @@ module rabbit_csr
     csr_rdata_o = 32'b0;
     unique case (csr_addr_i)
       CSR_MSTATUS  : csr_rdata_o = {19'b0, 2'b11, 3'b0, mstatus_mpie_q, 3'b0, mstatus_mie_q, 3'b0};
-      CSR_MISA     : csr_rdata_o = MISA_VALUE;
+      CSR_MISA     : csr_rdata_o = misa_value(CFG);
       CSR_MIE      : csr_rdata_o = mie_q;
       CSR_MIP      : csr_rdata_o = mip;
       CSR_MTVEC    : csr_rdata_o = mtvec_q;
diff --git a/rtl/cores/rabbit_common/rabbit_decoder.sv b/rtl/cores/rabbit_common/rabbit_decoder.sv
index 645caf0..adf3dfd 100644
--- a/rtl/cores/rabbit_common/rabbit_decoder.sv
+++ b/rtl/cores/rabbit_common/rabbit_decoder.sv
@@ -1,13 +1,15 @@
 // =============================================================================
 // rabbit_decoder — instruction bits -> decoded_t   (pure combinational)
 // =============================================================================
-// Supported: all of RV32I and RV32M, plus FENCE (a no-op) and WFI,
+// Supported: all of RV32I, RV32M if CFG.rv32m, plus FENCE (a no-op) and WFI,
 // ECALL, EBREAK, MRET and the six Zicsr instructions.
 // Anything else sets `illegal`; the EX stage turns that into a trap.
 // =============================================================================
 module rabbit_decoder
   import rabbit_pkg::*;
-(
+#(
+  parameter rabbit_cfg_t CFG = RABBIT_CFG
+) (
   input  logic [31:0] instr_i,
   output decoded_t    dec_o
 );
@@ -134,9 +136,12 @@ module rabbit_decoder
           3'b111: dec_o.alu_op = ALU_AND;
           default: ;
         endcase
-        // M extension (funct7 = 0000001): all eight funct3 values exist
-        if (funct7 == FUNCT7_MULDIV)
-          dec_o.is_muldiv = 1'b1;
+        // M extension (funct7 = 0000001): all eight funct3 values exist;
+        // without M (CFG.rv32m = 0) the whole group is illegal
+        if (funct7 == FUNCT7_MULDIV) begin
+          dec_o.is_muldiv = CFG.rv32m;
+          dec_o.illegal   = !CFG.rv32m;
+        end
         // only ADD/SUB and SRL/SRA have a second encoding (funct7 = 0100000)
         else if (funct7 == 7'b010_0000)
           dec_o.illegal = (funct3 != 3'b000) && (funct3 != 3'b101);
diff --git a/rtl/cores/rabbit_common/rabbit_execute.sv b/rtl/cores/rabbit_common/rabbit_execute.sv
index eb51652..efe5202 100644
--- a/rtl/cores/rabbit_common/rabbit_execute.sv
+++ b/rtl/cores/rabbit_common/rabbit_execute.sv
@@ -22,7 +22,7 @@
 // asks the pipeline to sleep (sleep_o) unless an enabled interrupt is
 // already pending. The pipeline stops fetching until wake_o.
 //
-// M extension (rabbit_muldiv): a multiply takes 2 cycles in execute, a
+// M extension (rabbit_muldiv, only if CFG.rv32m): a multiply takes 2 cycles in execute, a
 // divide 34, whatever the operands. Until it is done, busy_o = 1: the
 // pipeline must keep the instruction here, with the same operand values,
 // and let nothing younger move. An interrupt ends the wait at once: the
@@ -39,6 +39,7 @@
 module rabbit_execute
   import rabbit_pkg::*;
 #(
+  parameter rabbit_cfg_t CFG         = RABBIT_CFG,
   parameter logic [31:0] MTVEC_RESET = 32'h0,
   parameter logic [31:0] HART_ID     = 32'h0
 ) (
@@ -124,65 +125,72 @@ module rabbit_execute
   end
 
   // ---- M extension ---------------------------------------------------------------
+  // Without M the decoder never sets is_muldiv, so md_req stays 0 and none of
+  // this exists in the netlist.
   logic        md_req, md_done;
   logic [31:0] md_result;
   assign md_req = valid_i && dec_i.is_muldiv && !irq_pending;
   assign busy_o = md_req && !md_done;
 
+  if (CFG.rv32m) begin : g_muldiv
 `ifdef RABBIT_DIV_STEPS
-  localparam int unsigned DIV_STEPS = `RABBIT_DIV_STEPS;   // formal only, see rabbit_muldiv
+    localparam int unsigned DIV_STEPS = `RABBIT_DIV_STEPS;   // formal only, see rabbit_muldiv
 `else
-  localparam int unsigned DIV_STEPS = 32;
+    localparam int unsigned DIV_STEPS = 32;
 `endif
 
-  logic [31:0] md_value;
-  rabbit_muldiv #(.W(32), .DIV_STEPS(DIV_STEPS)) u_muldiv (
-    .clk_i, .rst_ni,
-    .en_i    (valid_i && dec_i.is_muldiv),
-    .req_i   (md_req),
-    .op_i    (dec_i.funct3),
-    .a_i     (rs1_i),
-    .b_i     (rs2_i),
-    .done_o  (md_done),
-    .result_o(md_value)
-  );
+    logic [31:0] md_value;
+    rabbit_muldiv #(.W(32), .DIV_STEPS(DIV_STEPS)) u_muldiv (
+      .clk_i, .rst_ni,
+      .en_i    (valid_i && dec_i.is_muldiv),
+      .req_i   (md_req),
+      .op_i    (dec_i.funct3),
+      .a_i     (rs1_i),
+      .b_i     (rs2_i),
+      .done_o  (md_done),
+      .result_o(md_value)
+    );
 
 `ifdef RISCV_FORMAL_ALTOPS
-  // riscv-formal cannot reason about real multiplication and division; with
-  // ALTOPS it expects these stand-in results instead (same timing). The real
-  // arithmetic is proven separately: dv/formal/rabbit/muldiv.
-  always_comb begin
-    unique case (dec_i.funct3)
-      3'd0:    md_result = (rs1_i + rs2_i) ^ 32'h5876_063e;   // MUL
-      3'd1:    md_result = (rs1_i + rs2_i) ^ 32'hf658_3fb7;   // MULH
-      3'd2:    md_result = (rs1_i - rs2_i) ^ 32'hecfb_e137;   // MULHSU
-      3'd3:    md_result = (rs1_i + rs2_i) ^ 32'h949c_e5e8;   // MULHU
-      3'd4:    md_result = (rs1_i - rs2_i) ^ 32'h7f85_29ec;   // DIV
-      3'd5:    md_result = (rs1_i - rs2_i) ^ 32'h10e8_fd70;   // DIVU
-      3'd6:    md_result = (rs1_i - rs2_i) ^ 32'h8da6_8fa5;   // REM
-      default: md_result = (rs1_i - rs2_i) ^ 32'h3138_d0e1;   // REMU
-    endcase
-  end
-  logic unused_md;
-  assign unused_md = ^md_value;
+    // riscv-formal cannot reason about real multiplication and division; with
+    // ALTOPS it expects these stand-in results instead (same timing). The real
+    // arithmetic is proven separately: dv/formal/rabbit/muldiv.
+    always_comb begin
+      unique case (dec_i.funct3)
+        3'd0:    md_result = (rs1_i + rs2_i) ^ 32'h5876_063e;   // MUL
+        3'd1:    md_result = (rs1_i + rs2_i) ^ 32'hf658_3fb7;   // MULH
+        3'd2:    md_result = (rs1_i - rs2_i) ^ 32'hecfb_e137;   // MULHSU
+        3'd3:    md_result = (rs1_i + rs2_i) ^ 32'h949c_e5e8;   // MULHU
+        3'd4:    md_result = (rs1_i - rs2_i) ^ 32'h7f85_29ec;   // DIV
+        3'd5:    md_result = (rs1_i - rs2_i) ^ 32'h10e8_fd70;   // DIVU
+        3'd6:    md_result = (rs1_i - rs2_i) ^ 32'h8da6_8fa5;   // REM
+        default: md_result = (rs1_i - rs2_i) ^ 32'h3138_d0e1;   // REMU
+      endcase
+    end
+    logic unused_md;
+    assign unused_md = ^md_value;
 `else
-  assign md_result = md_value;
+    assign md_result = md_value;
 `endif
 
 `ifndef SYNTHESIS
-  // The contract with the pipeline: the operands do not change while an M
-  // instruction is held here (also proven in dv/formal/rabbit/timing, M0).
-  logic        busy_q;
-  logic [31:0] rs1_q, rs2_q;
-  always_ff @(posedge clk_i or negedge rst_ni) begin
-    if (!rst_ni) busy_q <= 1'b0;
-    else begin
-      busy_q <= busy_o; rs1_q <= rs1_i; rs2_q <= rs2_i;
-      if (busy_q && md_req && (rs1_i != rs1_q || rs2_i != rs2_q))
-        $error("rabbit_execute: operands changed while a multiply/divide was held");
+    // The contract with the pipeline: the operands do not change while an M
+    // instruction is held here (also proven in dv/formal/rabbit/timing, M0).
+    logic        busy_q;
+    logic [31:0] rs1_q, rs2_q;
+    always_ff @(posedge clk_i or negedge rst_ni) begin
+      if (!rst_ni) busy_q <= 1'b0;
+      else begin
+        busy_q <= busy_o; rs1_q <= rs1_i; rs2_q <= rs2_i;
+        if (busy_q && md_req && (rs1_i != rs1_q || rs2_i != rs2_q))
+          $error("rabbit_execute: operands changed while a multiply/divide was held");
+      end
     end
-  end
 `endif
+  end else begin : g_no_muldiv
+    assign md_done   = 1'b1;
+    assign md_result = 32'b0;
+  end
 
   // ---- CSRs -------------------------------------------------------------------
   logic [31:0] csr_rdata, mtvec, mepc;
@@ -190,7 +198,7 @@ module rabbit_execute
   // 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 (
+  rabbit_csr #(.CFG(CFG), .MTVEC_RESET(MTVEC_RESET), .HART_ID(HART_ID)) u_csr (
     .clk_i, .rst_ni,
     .csr_valid_i  (valid_i && dec_i.is_csr && !irq_pending),
     .csr_addr_i   (instr_i[31:20]),
diff --git a/rtl/cores/rabbit_common/rabbit_pkg.sv b/rtl/cores/rabbit_common/rabbit_pkg.sv
index 9f089df..36b2457 100644
--- a/rtl/cores/rabbit_common/rabbit_pkg.sv
+++ b/rtl/cores/rabbit_common/rabbit_pkg.sv
@@ -8,6 +8,32 @@
 // =============================================================================
 package rabbit_pkg;
 
+  // ---------------------------------------------------------------------------
+  // Configuration: which optional parts of the ISA a core has.
+  //
+  // Every rabbit core takes one parameter CFG of this type and hands it to the
+  // blocks that need it. Its default, RABBIT_CFG, is set by the build:
+  //
+  //   configs/<name>.mk  (RV32M := 0)  ->  mk/config.mk  ->  -DRABBIT_RV32M=0
+  //
+  // These `RABBIT_* defines are read here and nowhere else in the RTL. A new
+  // option (C, F, vector, debug, ...) is one more field, one more define, and
+  // one more line in mk/config.mk (docs/dev: "adding a feature").
+  // ---------------------------------------------------------------------------
+  typedef struct packed {
+    logic rv32m;   // M: MUL*, DIV*, REM* (rabbit_muldiv). 0: they trap as illegal
+  } rabbit_cfg_t;
+
+`ifndef RABBIT_RV32M
+`define RABBIT_RV32M 1
+`endif
+  localparam rabbit_cfg_t RABBIT_CFG = '{rv32m: (`RABBIT_RV32M != 0)};
+
+  // misa: MXL = 1 (32-bit), I always, M if configured
+  function automatic logic [31:0] misa_value(rabbit_cfg_t cfg);
+    return 32'h4000_0100 | (cfg.rv32m ? 32'h0000_1000 : 32'h0);
+  endfunction
+
   // ---------------------------------------------------------------------------
   // RV32I major opcodes (instruction bits [6:0])
   // ---------------------------------------------------------------------------
@@ -96,8 +122,7 @@ package rabbit_pkg;
   localparam logic [11:0] CSR_MINSTRETH= 12'hB82;
   localparam logic [11:0] CSR_MHARTID  = 12'hF14;
 
-  // misa: MXL=1 (32-bit), extensions I and M
-  localparam logic [31:0] MISA_VALUE = 32'h4000_1100;
+  // misa: see misa_value() at the top (depends on the configuration)
 
   // ---------------------------------------------------------------------------
   // Interrupts. Line i of irq_i is bit i of mip and mie (RISC-V standard
diff --git a/sw/baremetal/Makefile b/sw/baremetal/Makefile
index cebe1e5..8a32e37 100644
--- a/sw/baremetal/Makefile
+++ b/sw/baremetal/Makefile
@@ -1,11 +1,10 @@
-# Build a bare-metal program for the selected core.
-#   make PROG=hello            -> build/$(CORE)/hello/hello.{elf,hex,dis}
-#   make PROG=hello CORE=ibex  (once an ibex adapter exists)
+# Build a bare-metal program for one SoC configuration (configs/).
+#   make PROG=hello                       -> build/cv32e40p/hello/hello.{elf,hex,dis}
+#   make PROG=muldiv CONFIG=rabbit5_rv32i -> build/rabbit5_rv32i/muldiv/...
 REPO  ?= $(abspath ../..)
-CORE  ?= cv32e40p
 PROG  ?= hello
 
-include $(REPO)/rtl/cores/$(CORE)/core.mk
+include $(REPO)/mk/config.mk
 
 CROSS ?= riscv64-unknown-elf-
 CC     = $(CROSS)gcc
@@ -13,7 +12,7 @@ OBJCOPY= $(CROSS)objcopy
 OBJDUMP= $(CROSS)objdump
 
 COMMON = $(REPO)/sw/baremetal/common
-OUT    = build/$(CORE)/$(PROG)
+OUT    = build/$(CONFIG)/$(PROG)
 
 # CORE_CFLAGS (core.mk): defines that describe a core's documented deviations
 CFLAGS  = $(CORE_CFLAGS) -march=$(CORE_MARCH) -mabi=$(CORE_MABI) -O2 -g -Wall -Wextra \
@@ -24,7 +23,7 @@ SRCS = $(COMMON)/crt0.S $(wildcard $(PROG)/*.c) $(wildcard $(PROG)/*.S)
 
 all: $(OUT)/$(PROG).hex $(OUT)/$(PROG).dis
 
-$(OUT)/$(PROG).elf: $(SRCS) $(COMMON)/link.ld $(COMMON)/rabbit_sim.h $(REPO)/rtl/cores/$(CORE)/core.mk
+$(OUT)/$(PROG).elf: $(SRCS) $(COMMON)/link.ld $(COMMON)/rabbit_sim.h $(CONFIG_DEPS)
 	@mkdir -p $(OUT)
 	$(CC) $(CFLAGS) $(SRCS) -o $@ $(LDFLAGS)
 
diff --git a/sw/baremetal/muldiv/main.c b/sw/baremetal/muldiv/main.c
index 4d48d5b..6ae6771 100644
--- a/sw/baremetal/muldiv/main.c
+++ b/sw/baremetal/muldiv/main.c
@@ -1,6 +1,8 @@
-/* M-extension self-test for the rabbit SoC (runs on every core; CV32E40P is
- * the reference).
+/* M-extension self-test for the rabbit SoC (runs on every configuration;
+ * CV32E40P is the reference).
  *
+ * With the M extension (compiled with -march=rv32im..., __riscv_mul defined):
+ *   0. misa says M
  *   1. corner cases of all eight instructions (x/0, -2^31/-1, signs, ...)
  *   2. pseudo-random operands, checked against a software model that uses
  *      only shifts and adds (no MUL/DIV instructions)
@@ -9,10 +11,23 @@
  *   4. an interrupt in the middle of a divide is taken at once, and the
  *      divide still gives the right result afterwards
  *
+ * Without it (a configuration with RV32M := 0, -march=rv32i...):
+ *   0. misa does not say M
+ *   5. each of the eight instructions traps as an illegal instruction
+ *      (mcause = 2, mtval = the instruction), and does not write rd
+ *   6. C code still multiplies and divides correctly (the compiler calls
+ *      libgcc's software routines instead)
+ *
  * Returns the number of failed checks (0 = PASS).
  */
 #include "rabbit_sim.h"
 
+#ifdef __riscv_mul
+#define HAS_M 1
+#else
+#define HAS_M 0
+#endif
+
 static int failures;
 
 static void fail(const char *what, uint32_t a, uint32_t b, uint32_t got, uint32_t exp) {
@@ -38,11 +53,17 @@ static void check(const char *name, uint32_t got, uint32_t expected) {
     sim_putc('\n');
 }
 
-/* ---- the eight instructions, exactly as written (no compiler tricks) ---- */
-#define OP(name) \
+/* ---- the eight instructions, exactly as encoded (no compiler tricks) ----
+ * Written with .insn (opcode OP = 0x33, funct7 = 1, funct3 = which one), so
+ * this file also assembles for a core without M, where they must trap. rd
+ * starts as RD_UNTOUCHED: an instruction that traps must leave it so. */
+#define RD_UNTOUCHED 0x5a5a5a5au
+#define OP(name, funct3) \
     static inline uint32_t op_##name(uint32_t a, uint32_t b) { \
-        uint32_t r; __asm__ volatile(#name " %0, %1, %2" : "=r"(r) : "r"(a), "r"(b)); return r; }
-OP(mul) OP(mulh) OP(mulhsu) OP(mulhu) OP(div) OP(divu) OP(rem) OP(remu)
+        uint32_t r = RD_UNTOUCHED; \
+        __asm__ volatile(".insn r 0x33, " #funct3 ", 1, %0, %1, %2" : "+r"(r) : "r"(a), "r"(b)); \
+        return r; }
+OP(mul, 0) OP(mulh, 1) OP(mulhsu, 2) OP(mulhu, 3) OP(div, 4) OP(divu, 5) OP(rem, 6) OP(remu, 7)
 
 /* ---- software model: shifts and adds only -------------------------------- */
 static uint64_t umul64(uint32_t a, uint32_t b) {
@@ -108,6 +129,7 @@ static uint32_t hw(int op, uint32_t a, uint32_t b) {
 
 static const char *const names[8] = {"mul", "mulh", "mulhsu", "mulhu", "div", "divu", "rem", "remu"};
 
+#if HAS_M
 /* ---- timing: cycles between two reads of the SoC cycle counter around one
  * instruction. The SoC counter (not mcycle) gives the same measurement on every
  * core: CV32E40P, for example, resets with mcycle stopped (mcountinhibit). */
@@ -119,14 +141,23 @@ static const char *const names[8] = {"mul", "mulh", "mulhsu", "mulhu", "div", "d
                          : "r"(RABBIT_SIM_CYCLE), "r"(a), "r"(b)); \
         (void)r; return t1 - t0; }
 TIMED(add) TIMED(mul) TIMED(mulhu) TIMED(div) TIMED(remu)
+#endif
 
-/* ---- interrupt during a divide ---------------------------------------------- */
+/* ---- trap handler: interrupts (test 4) and, without M, illegal M
+ * instructions (test 5) ------------------------------------------------------ */
 static volatile uint32_t n_irq, entry_cycle;
+static volatile uint32_t n_illegal, last_mtval;
 
 void __attribute__((interrupt("machine"))) trap_entry(void) {
     uint32_t now = sim_cycles();
     uint32_t cause = CSR_READ(mcause);
-    if (!(cause & MCAUSE_IRQ)) {                  /* an exception: stop the test */
+    if (!HAS_M && cause == 2) {                   /* illegal instruction: skip it */
+        n_illegal++;
+        last_mtval = CSR_READ(mtval);
+        CSR_WRITE(mepc, CSR_READ(mepc) + 4);
+        return;
+    }
+    if (!(cause & MCAUSE_IRQ)) {                  /* any other exception: stop the test */
         REG32(RABBIT_SIM_EXIT) = 0xDEAD0000u | (cause & 0x3ff);
         for (;;) { }
     }
@@ -138,11 +169,8 @@ void __attribute__((interrupt("machine"))) trap_entry(void) {
 static uint32_t xs = 0x2545F491u;                /* xorshift32 */
 static uint32_t rnd(void) { xs ^= xs << 13; xs ^= xs >> 17; xs ^= xs << 5; return xs; }
 
-int main(void) {
-    sim_puts("\nrt-rabbit: M extension test\n");
-    irq_global_disable();
-    CSR_WRITE(mie, 0);
-
+#if HAS_M
+static void test_with_m(void) {
     /* 1. corner cases --------------------------------------------------------- */
     static const uint32_t v[] = {0, 1, 7, 0x7fffffffu, 0x80000000u, 0x80000001u,
                                  0xfffffffeu, 0xffffffffu, 0x0000ffffu, 0xdeadbeefu};
@@ -213,7 +241,45 @@ int main(void) {
     check("irq taken during divide               ", n_irq, 1);
     check("  divide result after MRET            ", q, 10309278u);
     sim_puts("  raise -> handler (cycles) = "); sim_puthex(entry_cycle - t0); sim_putc('\n');
+}
+
+#else
+static void test_without_m(void) {
+    /* 5. every M instruction traps and leaves rd alone ------------------------- */
+    for (int op = 0; op < 8; op++) {
+        uint32_t before = n_illegal;
+        uint32_t r = hw(op, 6, 3);
+        uint32_t fixed = last_mtval & 0xfe00707fu;      /* funct7, funct3, opcode */
+        uint32_t want  = (1u << 25) | ((uint32_t)op << 12) | 0x33u;
+        if (n_illegal != before + 1 || fixed != want || r != RD_UNTOUCHED)
+            fail(names[op], n_illegal - before, last_mtval, r, want);
+    }
+    check("M instructions trapping as illegal    ", n_illegal, 8);
 
+    /* 6. C code multiplies and divides in software (libgcc) ------------------- */
+    int before = failures;
+    for (int n = 0; n < 48; n++) {
+        volatile uint32_t a = rnd(), b = rnd() >> (rnd() & 31);
+        if (b == 0) b = 1;
+        if (a * b != model(0, a, b)) fail("sw mul", a, b, a * b, model(0, a, b));
+        if (a / b != model(5, a, b)) fail("sw divu", a, b, a / b, model(5, a, b));
+        if (a % b != model(7, a, b)) fail("sw remu", a, b, a % b, model(7, a, b));
+    }
+    check("software mul/div (48 x 3) failures    ", failures - before, 0);
+}
+#endif
+
+int main(void) {
+    sim_puts(HAS_M ? "\nrt-rabbit: M extension test\n"
+                   : "\nrt-rabbit: M extension test (configuration without M)\n");
+    irq_global_disable();
+    CSR_WRITE(mie, 0);
+    check("misa.M                                ", (CSR_READ(misa) >> 12) & 1u, HAS_M);
+#if HAS_M
+    test_with_m();
+#else
+    test_without_m();
+#endif
     sim_puts(failures ? "RESULT: FAIL\n" : "RESULT: PASS\n");
     return failures;
 }
diff --git a/tools/check_all.sh b/tools/check_all.sh
index d17486b..708d16d 100755
--- a/tools/check_all.sh
+++ b/tools/check_all.sh
@@ -2,14 +2,15 @@
 # Reproduce every check of the rabbit cores on your own machine.
 #
 #   tools/check_all.sh                 quick + gls            (~10 min)
-#   tools/check_all.sh quick           lint, firmware on all 5 cores, muldiv exhaustive sim (~2 min)
-#   tools/check_all.sh gls             firmware on the gate-level netlists                  (~10 min)
-#   tools/check_all.sh formal          riscv-formal + timing + muldiv proof, both cores     (~60 min)
+#   tools/check_all.sh quick           lint + firmware on every configuration, muldiv exhaustive sim (~3 min)
+#   tools/check_all.sh gls             firmware on the gate-level netlists (rabbit configurations)  (~15 min)
+#   tools/check_all.sh formal          riscv-formal + timing + muldiv proof (rabbit configurations) (~70 min)
 #   tools/check_all.sh synth           sky130 area / delay table (needs the sky130 PDK)     (~1 min)
 #   tools/check_all.sh mutants         plant known bugs, check they are caught              (~30-60 min)
 #   tools/check_all.sh all             everything above                                     (~2-3 h)
 #
 # Several stages can be given: tools/check_all.sh quick formal
+# Configurations: every file in configs/ (CONFIGS="rabbit3 rabbit5_rv32i" to choose).
 # Logs: build/check_all/<stage>/...   Summary at the end; exit code 1 if anything failed.
 #
 # Needs (as in CI): verilator >= 5.03x, yosys with the slang frontend, sby +
@@ -20,6 +21,8 @@ REPO=$(cd "$(dirname "$0")/.." && pwd)
 cd "$REPO"
 
 STAGES=${*:-quick gls}
+CONFIGS=${CONFIGS:-$(ls configs/*.mk | xargs -n1 basename | sed 's/\.mk$//')}
+RABBIT_CONFIGS=$(printf '%s\n' $CONFIGS | grep '^rabbit' || true)
 [ "$STAGES" = all ] && STAGES="quick gls formal synth mutants"
 LOGS=build/check_all
 mkdir -p "$LOGS"
@@ -51,30 +54,30 @@ for stage in $STAGES; do
   echo "=== $stage"
   case $stage in
     quick)
-      for c in rabbit3 rabbit5 cv32e40p cve2 ibex; do
-        step "quick/lint-$c" "" make lint CORE=$c
+      for c in $CONFIGS; do
+        step "quick/lint-$c" "" make lint CONFIG=$c
         for p in hello irq muldiv; do
-          step "quick/sim-$c-$p" "RESULT: PASS" make soc-sim CORE=$c PROG=$p
+          step "quick/sim-$c-$p" "RESULT: PASS" make soc-sim CONFIG=$c PROG=$p
         done
       done
       step "quick/muldiv-exhaustive-8bit" "RESULT: PASS" make -C dv/formal/rabbit muldiv-sim
       ;;
     gls)
-      for c in rabbit3 rabbit5; do
+      for c in $RABBIT_CONFIGS; do
         for p in hello irq muldiv; do
-          step "gls/$c-$p" "RESULT: PASS" make gls-smoke CORE=$c PROG=$p
+          step "gls/$c-$p" "RESULT: PASS" make gls-smoke CONFIG=$c PROG=$p
         done
       done
       ;;
     formal)
       step "formal/muldiv-unit" "" make -C dv/formal/rabbit muldiv
-      for c in rabbit5 rabbit3; do
-        step "formal/$c-riscv-formal" "53/53 checks PASS" make -C dv/formal/rabbit CORE=$c riscv-formal
-        step "formal/$c-timing" "" make -C dv/formal/rabbit CORE=$c timing
+      for c in $RABBIT_CONFIGS; do
+        step "formal/$c-riscv-formal" "checks PASS" make -C dv/formal/rabbit CONFIG=$c riscv-formal
+        step "formal/$c-timing" "" make -C dv/formal/rabbit CONFIG=$c timing
       done
       ;;
     synth)
-      step "synth/sky130" "" tools/synth_sky130.sh
+      step "synth/sky130" "" tools/synth_sky130.sh $CONFIGS
       cat "$LOGS/synth/sky130.log"
       ;;
     mutants)
diff --git a/tools/core_sources.sh b/tools/core_sources.sh
index c15734d..64ae3e4 100755
--- a/tools/core_sources.sh
+++ b/tools/core_sources.sh
@@ -1,18 +1,21 @@
 #!/usr/bin/env bash
-# Print the read_slang arguments (include dirs + files) for one core, from its
-# rtl/cores/<core>/files.f, with the few vendor workarounds Yosys' slang
-# frontend needs. Used by tools/synth_sky130.sh and asic/orfs.
+# Print the read_slang arguments (include dirs, files, configuration defines)
+# for one SoC configuration, from rtl/cores/<core>/files.f, with the few vendor
+# workarounds Yosys' slang frontend needs. Used by tools/synth_sky130.sh and
+# asic/orfs/run.sh.
 #
-#   tools/core_sources.sh <core> <scratch dir for patched copies>
+#   tools/core_sources.sh <config> <scratch dir for patched copies>
+#   (<config>: a file in configs/, e.g. rabbit5 or rabbit5_rv32i)
 set -euo pipefail
 REPO=$(cd "$(dirname "$0")/.." && pwd)
-core=$1 tmp=$2
+config=$1 tmp=$2
 mkdir -p "$tmp"
+eval "$(make -s -C "$REPO" config-vars CONFIG="$config")"   # sets CORE, CONFIG_DEFINES
 
 # files.f: drop comments, expand ${REPO}, turn +incdir+ into -I
-SRC=$(grep -v '^//' "$REPO/rtl/cores/$core/files.f" | sed "s|\${REPO}|$REPO|" | sed 's|^+incdir+|-I |' | tr '\n' ' ')
+SRC=$(grep -v '^//' "$REPO/rtl/cores/$CORE/files.f" | sed "s|\${REPO}|$REPO|" | sed 's|^+incdir+|-I |' | tr '\n' ' ')
 
-if [ "$core" = ibex ]; then
+if [ "$CORE" = ibex ]; then
   # slang cannot elaborate a module-level variable whose initializer reads
   # nets (ibex_top.sv, a lint-only "unused" signal). Use a copy where it is a
   # plain assign; the vendor file itself is not touched.
@@ -20,4 +23,4 @@ if [ "$core" = ibex ]; then
       "$REPO/third_party/ibex/rtl/ibex_top.sv" > "$tmp/ibex_top.sv"
   SRC=${SRC//$REPO\/third_party\/ibex\/rtl\/ibex_top.sv/$tmp/ibex_top.sv}
 fi
-echo "$SRC"
+echo "$SRC $CONFIG_DEFINES"
diff --git a/tools/mutants.py b/tools/mutants.py
index c934489..3ef4dde 100755
--- a/tools/mutants.py
+++ b/tools/mutants.py
@@ -37,7 +37,7 @@ def sby(task):
 def rvf(core, check):
     """One riscv-formal check; the verdict is read from its status file."""
     return {
-        "cmd": ["make", f"CORE={core}", "check", f"C={check}"],
+        "cmd": ["make", f"CONFIG={core}", "check", f"C={check}"],
         "cwd": "dv/formal/rabbit",
         "status": f"dv/formal/rabbit/build/{core}/riscv-formal/cores/{core}/checks/{check}/status",
     }
@@ -91,6 +91,8 @@ def ignore(folder, names):
                      if (n == "muldiv" or n.startswith("muldiv_")) and (Path(folder) / n).is_dir()}
         return skip
     shutil.copytree(REPO / "rtl", dst / "rtl", ignore=ignore)
+    shutil.copytree(REPO / "configs", dst / "configs")
+    shutil.copytree(REPO / "mk", dst / "mk")
     shutil.copytree(REPO / "dv" / "formal" / "rabbit", dst / "dv" / "formal" / "rabbit", ignore=ignore)
     (dst / "third_party").mkdir()
     (dst / "third_party" / "riscv-formal").symlink_to(REPO / "third_party" / "riscv-formal")
diff --git a/tools/synth_sky130.sh b/tools/synth_sky130.sh
index 6edf109..f73c686 100755
--- a/tools/synth_sky130.sh
+++ b/tools/synth_sky130.sh
@@ -1,14 +1,14 @@
 #!/usr/bin/env bash
-# Area and longest combinational path of the cores on sky130 (Yosys + ABC).
+# Area and longest combinational path of SoC configurations on sky130 (Yosys + ABC).
 #
-#   tools/synth_sky130.sh                 rabbit3 rabbit5 cv32e40p cve2 ibex
-#   tools/synth_sky130.sh rabbit3         one core
+#   tools/synth_sky130.sh                 every configuration in configs/
+#   tools/synth_sky130.sh rabbit3 rabbit3_rv32i     selected ones
 #
 # Finds the sky130_fd_sc_hd typical-corner liberty file in $SKY130_LIB, or
 # under $PDK_ROOT, or under ~/.ciel / ~/.volare (ciel / volare installs).
 # Numbers are a quick comparison, not sign-off: no wires, no placement, and
 # ABC's delay varies by about +-0.6 ns between runs of nearly the same RTL.
-# Logs: build/synth_sky130/<core>.log
+# Logs: build/synth_sky130/<config>.log
 set -euo pipefail
 REPO=$(cd "$(dirname "$0")/.." && pwd)
 cd "$REPO"
@@ -28,10 +28,10 @@ fi
 
 OUT=build/synth_sky130
 mkdir -p "$OUT"
-CORES=${*:-rabbit3 rabbit5 cv32e40p cve2 ibex}
+CONFIGS=${*:-$(ls configs/*.mk | xargs -n1 basename | sed 's/\.mk$//')}
 
-printf '%-10s %14s %12s %12s\n' core "area um2" "of it flops" "delay ns"
-for c in $CORES; do
+printf '%-16s %14s %12s %12s\n' config "area um2" "of it flops" "delay ns"
+for c in $CONFIGS; do
   SRC=$(tools/core_sources.sh "$c" "$OUT/src_$c")
   yosys -p "read_slang $SRC --top rabbit_cpu -DSYNTHESIS; \
             synth -top rabbit_cpu -booth -flatten; \
@@ -41,5 +41,5 @@ for c in $CORES; do
   area=$(grep 'Chip area for module' "$OUT/$c.log" | tail -1 | awk '{print $NF}')
   seq=$(grep 'used for sequential elements' "$OUT/$c.log" | tail -1 | awk '{print $(NF-1)}')
   dly=$(grep -oE 'Delay *= *[0-9.]+ ps' "$OUT/$c.log" | tail -1 | grep -oE '[0-9.]+')
-  printf '%-10s %14.0f %12.0f %12.2f\n' "$c" "$area" "$seq" "$(echo "$dly / 1000" | bc -l)"
+  printf '%-16s %14.0f %12.0f %12.2f\n' "$c" "$area" "$seq" "$(echo "$dly / 1000" | bc -l)"
 done