diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0a5f60f..096cd90 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,7 +1,12 @@
 name: ci
 
+# Fast checks only (each job about a minute): runs on every pull request and
+# on main. Formal proofs, gate-level simulation and mutation tests take much
+# longer: they are in deep-verify.yml (Actions tab -> "deep-verify" -> Run
+# workflow) and in tools/check_all.sh on your own machine.
 on:
   push:
+    branches: [main]      # branches are checked through their pull request (no double runs)
   pull_request:
   workflow_dispatch:
 
@@ -21,7 +26,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [cv32e40p, rabbit3, rabbit5]
+        core: [cv32e40p, cve2, ibex, rabbit3, rabbit5]
     steps:
       - uses: actions/checkout@v4
         with: { submodules: recursive }
@@ -34,7 +39,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [cv32e40p, rabbit3, rabbit5]
+        core: [cv32e40p, cve2, ibex, rabbit3, rabbit5]
         # irq: interrupt self-test; cv32e40p is the reference the rabbits must match
         prog: [hello, irq, muldiv]
     steps:
@@ -69,74 +74,14 @@ jobs:
       - working-directory: hw_ip/sim
         run: uv run make TARGET=${{ matrix.target }}   # non-zero exit on any failed test
 
-  # riscv-formal (53 checks, RV32IM) + timing properties + the multiply/divide
-  # unit proof (dv/formal/rabbit/muldiv), for each of our own cores.
-  formal:
-    runs-on: ubuntu-24.04
-    # locally: riscv-formal 3 min (rabbit3) / 0.5 min (rabbit5), timing ~15 min each
-    timeout-minutes: 90
-    strategy:
-      fail-fast: false
-      matrix:
-        core: [rabbit3, rabbit5]
-    steps:
-      - uses: actions/checkout@v4
-        with: { submodules: recursive }
-      - uses: YosysHQ/setup-oss-cad-suite@v3
-        with: { version: "2026-11-04" }     # pinned: yosys, sby, boolector
-      - run: yosys -V && sby --version
-      - run: make formal CORE=${{ matrix.core }}
-      - uses: actions/upload-artifact@v4
-        if: failure()
-        with:
-          name: formal-results-${{ matrix.core }}
-          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
-
-  # Gate-level smoke test: Yosys builds the netlist, the pinned Verilator image runs it.
-  gls-netlist:
-    runs-on: ubuntu-24.04
-    strategy:
-      matrix:
-        core: [rabbit3, rabbit5]
-    steps:
-      - uses: actions/checkout@v4
-      - uses: YosysHQ/setup-oss-cad-suite@v3
-        with: { version: "2026-11-04" }
-      - run: make gls-netlist CORE=${{ matrix.core }}
-      - uses: actions/upload-artifact@v4
-        with:
-          name: gls-netlist-${{ matrix.core }}
-          path: build/gls/${{ matrix.core }}
-
-  gls-smoke:
-    needs: gls-netlist
+  # Exhaustive multiply/divide check at 8 bits (all 524 288 instructions), ~1 s.
+  # The heavy proofs and gate-level runs are in deep-verify.yml (run on demand).
+  muldiv-exhaustive:
     runs-on: ubuntu-24.04
     container: { image: "verilator/verilator:v5.054", options: --entrypoint "" }
-    strategy:
-      fail-fast: false
-      matrix:
-        core: [rabbit3, rabbit5]
     steps:
-      - name: RISC-V GCC
-        run: apt-get update -q && apt-get install -y -q gcc-riscv64-unknown-elf libpython3.12-dev
       - uses: actions/checkout@v4
-      - uses: astral-sh/setup-uv@v6
-      - uses: actions/download-artifact@v4
-        with:
-          name: gls-netlist-${{ matrix.core }}
-          path: build/gls/${{ matrix.core }}
-      - run: uv sync
-      - working-directory: dv/cocotb/soc
-        run: uv run make CORE=${{ matrix.core }} PROG=hello GLS=1
-      - working-directory: dv/cocotb/soc
-        run: uv run make CORE=${{ matrix.core }} 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: make -C dv/formal/rabbit muldiv-sim
 
   rma-smoke:
     runs-on: ubuntu-24.04
diff --git a/.github/workflows/deep-verify.yml b/.github/workflows/deep-verify.yml
new file mode 100644
index 0000000..b443b37
--- /dev/null
+++ b/.github/workflows/deep-verify.yml
@@ -0,0 +1,103 @@
+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)
+#   mutants  plant known bugs, check each is caught (~45 min)
+#   all      everything
+on:
+  workflow_dispatch:
+    inputs:
+      what:
+        description: "what to run"
+        type: choice
+        options: [all, formal, gls, mutants]
+        default: all
+
+concurrency:
+  group: deep-verify-${{ github.ref }}
+  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.
+  formal:
+    if: ${{ inputs.what == 'all' || inputs.what == 'formal' }}
+    runs-on: ubuntu-24.04
+    # GitHub runners: ~7-10 min per core (2026-11-07)
+    timeout-minutes: 90
+    strategy:
+      fail-fast: false
+      matrix:
+        core: [rabbit3, rabbit5]
+    steps:
+      - uses: actions/checkout@v4
+        with: { submodules: recursive }
+      - uses: YosysHQ/setup-oss-cad-suite@v3
+        with: { version: "2026-11-04" }     # pinned: yosys, sby, boolector
+      - run: yosys -V && sby --version
+      - run: make formal CORE=${{ matrix.core }}
+      - uses: actions/upload-artifact@v4
+        if: failure()
+        with:
+          name: formal-results-${{ matrix.core }}
+          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
+
+  # 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]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: YosysHQ/setup-oss-cad-suite@v3
+        with: { version: "2026-11-04" }
+      - run: make gls-netlist CORE=${{ matrix.core }}
+      - uses: actions/upload-artifact@v4
+        with:
+          name: gls-netlist-${{ matrix.core }}
+          path: build/gls/${{ matrix.core }}
+
+  gls-smoke:
+    needs: gls-netlist
+    runs-on: ubuntu-24.04
+    container: { image: "verilator/verilator:v5.054", options: --entrypoint "" }
+    strategy:
+      fail-fast: false
+      matrix:
+        core: [rabbit3, rabbit5]
+    steps:
+      - name: RISC-V GCC
+        run: apt-get update -q && apt-get install -y -q gcc-riscv64-unknown-elf libpython3.12-dev
+      - uses: actions/checkout@v4
+      - uses: astral-sh/setup-uv@v6
+      - uses: actions/download-artifact@v4
+        with:
+          name: gls-netlist-${{ matrix.core }}
+          path: build/gls/${{ matrix.core }}
+      - run: uv sync
+      - working-directory: dv/cocotb/soc
+        run: uv run make CORE=${{ matrix.core }} PROG=hello GLS=1
+      - working-directory: dv/cocotb/soc
+        run: uv run make CORE=${{ matrix.core }} 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
+
+  mutants:
+    if: ${{ inputs.what == 'all' || inputs.what == 'mutants' }}
+    runs-on: ubuntu-24.04
+    timeout-minutes: 180
+    steps:
+      - uses: actions/checkout@v4
+        with: { submodules: recursive }
+      - uses: YosysHQ/setup-oss-cad-suite@v3
+        with: { version: "2026-11-04" }
+      - run: python3 tools/mutants.py --baseline
diff --git a/.gitmodules b/.gitmodules
index 19b1c5c..adfad3a 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -4,3 +4,9 @@
 [submodule "third_party/riscv-formal"]
 	path = third_party/riscv-formal
 	url = https://github.com/YosysHQ/riscv-formal.git
+[submodule "third_party/cve2"]
+	path = third_party/cve2
+	url = https://github.com/openhwgroup/cve2.git
+[submodule "third_party/ibex"]
+	path = third_party/ibex
+	url = https://github.com/lowRISC/ibex.git
diff --git a/README.md b/README.md
index 0bf7e44..ded474e 100644
--- a/README.md
+++ b/README.md
@@ -30,10 +30,10 @@ behind the numbers in the docs and prints a PASS/FAIL summary:
 
 | Stage | What | Time |
 |---|---|---|
-| `quick` | lint, `hello` / `irq` / `muldiv` firmware on rabbit3, rabbit5, CV32E40P; exhaustive 8-bit muldiv simulation | ~1 min |
+| `quick` | lint, `hello` / `irq` / `muldiv` firmware on rabbit3, rabbit5, CV32E40P, CVE2, Ibex; exhaustive 8-bit muldiv simulation | ~2 min |
 | `gls` | the same firmware on the gate-level netlists | ~10 min |
 | `formal` | riscv-formal, timing properties, muldiv unit proof, both rabbit cores | ~60 min |
-| `synth` | sky130 area / delay table (`tools/synth_sky130.sh`, needs the PDK) | ~1 min |
+| `synth` | sky130 area / delay table of all five cores (`tools/synth_sky130.sh`, needs the PDK) | ~2 min |
 | `mutants` | plants known bugs in a copy and checks each is caught (`tools/mutants.py`) | ~30–60 min |
 
 Default is `quick gls`; `tools/check_all.sh all` runs everything. Tools
diff --git a/docs/GETTING_STARTED.md b/docs/GETTING_STARTED.md
index 0c06aca..1e23e3f 100644
--- a/docs/GETTING_STARTED.md
+++ b/docs/GETTING_STARTED.md
@@ -45,7 +45,7 @@ fw|   misa  = 0x40001104        <- RV32, extensions I, M, C
 fw|   [ok]   mul     = 0x068c94ef
 ...
 fw| RESULT: PASS
-hello finished after 3450 cycles, exit code 0x00000000
+hello finished after 3447 cycles, exit code 0x00000000
 ```
 
 Good signals to put in the waveform viewer first:
diff --git a/docs/STATUS.md b/docs/STATUS.md
index d0110c3..cf02b08 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -4,19 +4,21 @@
 
 | Item | Command | Result |
 |---|---|---|
-| CV32E40P (v1.8.3, RV32IMC) in `rabbit_soc_sim`, Verilator | `make soc-sim` | hello: 6/6 checks pass, 3450 cycles |
+| CV32E40P (v1.8.3, RV32IMC) in `rabbit_soc_sim`, Verilator | `make soc-sim` | hello: 6/6 checks pass, 3447 cycles |
 | Lint of our RTL (`-Wall`, vendor code excluded) | `make lint` | clean |
 | hw_ip cocotb tests | `make ip-test` | 10 targets, 19 tests pass |
 | rma_analysis examples | `make rma-smoke` | 11 run, 1 expected failure |
-| GitHub Actions | `.github/workflows/ci.yml` | lint, soc-sim matrix, ip-test matrix, rma-smoke, formal, GLS |
+| GitHub Actions | `.github/workflows/ci.yml` (every PR, ~1 min jobs) + `deep-verify.yml` (on demand) | ci: lint, soc-sim (5 cores), ip-test, rma-smoke, muldiv exhaustive; deep-verify: formal, GLS, mutants |
 | 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) |
 
 ## Own cores: rabbit3 and rabbit5 (shared blocks in rtl/cores/rabbit_common)
 
 | Item | rabbit3 (3-stage) | rabbit5 (5-stage) |
 |---|---|---|
 | ISA | RV32IM + Zicsr | RV32IM + Zicsr |
-| hello (`make soc-sim CORE=...`) | PASS, 2756 cycles | PASS, 3471 cycles |
+| hello (`make soc-sim CORE=...`) | PASS, 2758 cycles | PASS, 3473 cycles |
 | interrupts + WFI (`PROG=irq`, same test passes on cv32e40p) | PASS, 7448 cycles | PASS, 9025 cycles |
 | M extension (`PROG=muldiv`, same test passes on cv32e40p) | PASS; MUL 2 cycles, DIV 34, data-independent | same |
 | riscv-formal (`make formal CORE=...`, M via ALTOPS) | 53/53 | 53/53 |
diff --git a/dv/cocotb/soc/test_soc.py b/dv/cocotb/soc/test_soc.py
index a11086d..ead7e44 100644
--- a/dv/cocotb/soc/test_soc.py
+++ b/dv/cocotb/soc/test_soc.py
@@ -8,7 +8,7 @@
 
 import cocotb
 from cocotb.clock import Clock
-from cocotb.triggers import ClockCycles, RisingEdge
+from cocotb.triggers import ClockCycles, RisingEdge, Timer
 
 MAX_CYCLES = int(os.environ.get("RABBIT_MAX_CYCLES", "1000000"))
 
@@ -17,6 +17,12 @@ async def run_firmware(dut, max_cycles: int = MAX_CYCLES):
     """Reset the SoC, run until EXIT is written, return (exit_code, console, cycles)."""
     cocotb.start_soon(Clock(dut.clk_i, 10, unit="ns").start())
     dut.irq_i.value = 0
+    # Give rst_ni a real falling edge. Starting at 0 there is no negedge, so an
+    # asynchronous reset only acts at a clock edge - and a core that gates its
+    # own clock during reset (CVE2, Ibex) then never resets those registers in
+    # Verilator (silicon would: there the reset is level-sensitive).
+    dut.rst_ni.value = 1
+    await Timer(1, unit="ns")
     dut.rst_ni.value = 0
     await ClockCycles(dut.clk_i, 5)
     dut.rst_ni.value = 1
diff --git a/rtl/cores/README.md b/rtl/cores/README.md
index bf635ad..5419e46 100644
--- a/rtl/cores/README.md
+++ b/rtl/cores/README.md
@@ -8,7 +8,7 @@ support lives in its own sub-directory and provides:
 |---|---|
 | `rabbit_cpu.sv` | Adapter: instantiates the real core and maps it onto the contract below |
 | `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.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`).
 Only one `rabbit_cpu` is compiled per build, so no `ifdef` soup is needed.
@@ -54,12 +54,37 @@ adapter, in `rtl/soc/`.
 | Dir | Core | Status | Notes |
 |---|---|---|---|
 | `cv32e40p/` | OpenHW CV32E40P v1.8.3 (RV32IMC, 4-stage) | **working** | Baseline for Y1 |
-| `ibex/` | lowRISC Ibex | planned | Same OBI-like bus, 2/3-stage; good for area comparison |
+| `cve2/` | OpenHW CVE2 / CV32E20 (RV32IMC, 2-stage, Ibex-derived), pinned commit | **working** | Reference for comparison; fast interrupts: lowest line first |
+| `ibex/` | lowRISC Ibex "small" (RV32IMC, 2-stage, fast multiplier), pinned commit | **working** | Reference for comparison; 15 fast lines (16..30), lowest first |
 | `cv32e40x/` | OpenHW CV32E40X | planned | Brings CV-X-IF for the vector/NN coprocessor |
 | `rabbit3/` | Our own 3-stage RV32IM core (F/X/W) — **start here** | **working** | riscv-formal 53/53, timing + interrupt properties, interrupts + WFI, fixed-latency M, GLS smoke |
 | `rabbit5/` | Our own 5-stage, timing-predictable RV32IM core | **working** | riscv-formal 53/53, timing + interrupt properties, interrupts + WFI, fixed-latency M, GLS smoke |
 | `rabbit_common/` | Blocks shared by rabbit3 and rabbit5 (decoder, ALU, regfile, CSRs, execute, RVFI) | — | not a core; listed in each core's `files.f` |
 
+## Same flow, five cores (2026-11-07)
+
+Every number from our own scripts (`tools/synth_sky130.sh`, `make soc-sim`),
+same firmware, same SoC, same sky130 typical-corner library, Yosys
+`synth -booth` + ABC, no wires (a comparison, not sign-off; ABC's delay moves
+by about ±0.6 ns between runs of nearly identical RTL).
+
+| Core | ISA | Area µm² (of it flops) | Longest path | `hello` cycles | MUL / MULH / DIV extra cycles | interrupt during a divide → handler |
+|---|---|---|---|---|---|---|
+| rabbit3 | RV32IM | **114 853** (44 981) | 10.0–10.7 ns | **2758** | 1 / 1 / 33, any data | **14** |
+| rabbit5 | RV32IM | 126 549 (52 338) | 9.0–9.5 ns | 3473 | 1 / 1 / 33, any data | 17 |
+| Ibex (small) | RV32IMC | 124 899 (48 798) | **6.4 ns** | 3984 | 2 / 3 / 36 | 20 |
+| CVE2 | RV32IMC | 128 964 (48 107) | 6.5 ns | 3984 | 2 / 3 / 36 | 20 |
+| CV32E40P | RV32IMC | 170 298 (53 794) | 6.9 ns | 3447 | 0 / 4 / 31 (depends on data) | 41 (finishes the divide) |
+
+Reading it honestly: rabbit3 is the smallest and both rabbits need the fewest
+cycles, but their clock period is ~1.5x longer, so Ibex/CVE2 run `hello` in
+less *time* today. The rabbit critical path is instruction word → decode /
+trap logic → enable of the 64-bit `minstret`/`mcycle` counters, not the
+pipeline itself: fixing it is the next step. Ibex and CVE2 also abandon a
+divide on an interrupt; what only the rabbit cores have is the *proof*
+(latency bound, data-independent M timing). The Ibex/CVE2/CV32E40P numbers
+include the C extension (decompressor, aligner); the rabbits have none.
+
 The contract will grow (v1) with an optional **coprocessor port** (CV-X-IF
 style) and an optional **RVFI trace port** for lockstep checking against Spike/Sail.
 (rabbit5 already has RVFI on `rabbit5_core`; the adapter leaves it unconnected.)
diff --git a/rtl/cores/cve2/README.md b/rtl/cores/cve2/README.md
new file mode 100644
index 0000000..dab6611
--- /dev/null
+++ b/rtl/cores/cve2/README.md
@@ -0,0 +1,27 @@
+# cve2 — OpenHW CVE2 (CV32E20) as a reference core
+
+`third_party/cve2` (submodule, pinned commit), wrapped by `rabbit_cpu.sv`.
+CVE2 is OpenHW's industrial-grade derivative of an early Ibex: 2 stages,
+RV32IMC + Zicsr. Used for comparison (`../README.md`), not developed here.
+
+Configuration: fast multiplier (MUL 3, MULH 4, DIV 37 cycles), no
+X-interface, no extra performance counters (MHPMCounterNum = 0, as in the
+Ibex adapter, so the area comparison is fair).
+
+Deviations from the `rabbit_cpu` contract (documented in the adapter):
+- first fetch AT `boot_addr`, vectored `mtvec` at `boot_addr[31:8]` →
+  `boot_addr_i = BOOT_ADDR`, which must lie in MTVEC_ADDR's 256-byte block;
+- fast interrupt lines 16..31: the **lowest** line wins
+  (`CORE_CFLAGS := -DIRQ_FAST_LOW_LINE_FIRST`);
+- no `irq_ack_o` / `irq_id_o` (tied to 0).
+
+Bringing it up found a bug in **our** testbench: reset started low, so in
+Verilator an asynchronous reset only acted at clock edges, and CVE2 gates its
+own clock during reset — its privilege level stayed 0 (user mode) and the
+first `csrr misa` trapped. `dv/cocotb/soc/test_soc.py` now gives reset a real
+falling edge.
+
+```bash
+make soc-sim CORE=cve2 PROG=irq
+tools/synth_sky130.sh cve2
+```
diff --git a/rtl/cores/cve2/core.mk b/rtl/cores/cve2/core.mk
new file mode 100644
index 0000000..732f7cf
--- /dev/null
+++ b/rtl/cores/cve2/core.mk
@@ -0,0 +1,8 @@
+# Per-core build settings, included by the top-level and dv Makefiles.
+CORE_MARCH       := rv32imc_zicsr
+CORE_MABI        := ilp32
+# Vendor code: keep warnings non-fatal.
+CORE_VERILATOR_FLAGS := -Wno-fatal
+# Contract deviation: among the fast interrupt lines 16..31 the LOWEST line
+# wins (CV32E40P and the rabbit cores: the highest). sw/baremetal/irq expects it.
+CORE_CFLAGS      := -DIRQ_FAST_LOW_LINE_FIRST
diff --git a/rtl/cores/cve2/files.f b/rtl/cores/cve2/files.f
new file mode 100644
index 0000000..8c07538
--- /dev/null
+++ b/rtl/cores/cve2/files.f
@@ -0,0 +1,31 @@
+// OpenHW CVE2 (third_party/cve2, pinned commit) + rabbit_cpu adapter.
+// From cve2's cv32e20_manifest.flist, without the tracer. ${REPO} is expanded by make.
++incdir+${REPO}/third_party/cve2/rtl
++incdir+${REPO}/third_party/cve2/shared/rtl
++incdir+${REPO}/third_party/cve2/vendor/lowrisc_ip/ip/prim/rtl
++incdir+${REPO}/third_party/cve2/vendor/lowrisc_ip/dv/sv/dv_utils
+${REPO}/third_party/cve2/rtl/cve2_pkg.sv
+${REPO}/third_party/cve2/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_pkg.sv
+${REPO}/third_party/cve2/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_pkg.sv
+${REPO}/third_party/cve2/rtl/cve2_alu.sv
+${REPO}/third_party/cve2/rtl/cve2_compressed_decoder.sv
+${REPO}/third_party/cve2/rtl/cve2_controller.sv
+${REPO}/third_party/cve2/rtl/cve2_cs_registers.sv
+${REPO}/third_party/cve2/rtl/cve2_csr.sv
+${REPO}/third_party/cve2/rtl/cve2_counter.sv
+${REPO}/third_party/cve2/rtl/cve2_decoder.sv
+${REPO}/third_party/cve2/rtl/cve2_ex_block.sv
+${REPO}/third_party/cve2/rtl/cve2_fetch_fifo.sv
+${REPO}/third_party/cve2/rtl/cve2_id_stage.sv
+${REPO}/third_party/cve2/rtl/cve2_if_stage.sv
+${REPO}/third_party/cve2/rtl/cve2_load_store_unit.sv
+${REPO}/third_party/cve2/rtl/cve2_multdiv_fast.sv
+${REPO}/third_party/cve2/rtl/cve2_multdiv_slow.sv
+${REPO}/third_party/cve2/rtl/cve2_prefetch_buffer.sv
+${REPO}/third_party/cve2/rtl/cve2_pmp.sv
+${REPO}/third_party/cve2/rtl/cve2_register_file_ff.sv
+${REPO}/third_party/cve2/rtl/cve2_wb.sv
+${REPO}/third_party/cve2/rtl/cve2_core.sv
+${REPO}/third_party/cve2/rtl/cve2_top.sv
+${REPO}/third_party/cve2/rtl/cve2_clock_gate.sv
+${REPO}/rtl/cores/cve2/rabbit_cpu.sv
diff --git a/rtl/cores/cve2/rabbit_cpu.sv b/rtl/cores/cve2/rabbit_cpu.sv
new file mode 100644
index 0000000..892b90b
--- /dev/null
+++ b/rtl/cores/cve2/rabbit_cpu.sv
@@ -0,0 +1,108 @@
+// rabbit_cpu adapter for OpenHW CVE2 (third_party/cve2, pinned commit; the
+// "CV32E20": Ibex-derived 2-stage RV32IMC core).
+// Configuration: RV32IMC + Zicsr, fast multiplier (RV32MFast), no X-interface,
+// no extra performance counters (MHPMCounterNum = 0).
+// See rtl/cores/README.md for the port contract.
+//
+// Differences from the contract (documented, not hidden):
+// - CVE2 starts fetching AT boot_addr and puts the vectored mtvec at
+//   boot_addr[31:8]; with the contract defaults (BOOT_ADDR 0x80, MTVEC 0x0)
+//   both line up. Other combinations are rejected below.
+// - fast interrupts 16..31: the lowest line has the highest priority.
+// - irq_ack_o / irq_id_o do not exist on CVE2: tied to 0.
+module rabbit_cpu #(
+    parameter logic [31:0] BOOT_ADDR  = 32'h0000_0080,
+    parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000
+) (
+    input  logic        clk_i,
+    input  logic        rst_ni,
+    input  logic        fetch_enable_i,
+
+    output logic        instr_req_o,
+    input  logic        instr_gnt_i,
+    input  logic        instr_rvalid_i,
+    output logic [31:0] instr_addr_o,
+    input  logic [31:0] instr_rdata_i,
+
+    output logic        data_req_o,
+    input  logic        data_gnt_i,
+    input  logic        data_rvalid_i,
+    output logic        data_we_o,
+    output logic [ 3:0] data_be_o,
+    output logic [31:0] data_addr_o,
+    output logic [31:0] data_wdata_o,
+    input  logic [31:0] data_rdata_i,
+
+    input  logic [31:0] irq_i,
+    output logic        irq_ack_o,
+    output logic [ 4:0] irq_id_o,
+
+    input  logic        debug_req_i,
+    output logic        core_sleep_o
+);
+
+  if (MTVEC_ADDR[7:0] != 8'h00 || BOOT_ADDR[31:8] != MTVEC_ADDR[31:8]) begin : g_bad_addr
+    $error("cve2 adapter: needs MTVEC_ADDR 256-byte aligned and BOOT_ADDR in the same 256-byte block");
+  end
+
+  assign irq_ack_o = 1'b0;
+  assign irq_id_o  = '0;
+
+  cve2_top #(
+      .MHPMCounterNum(0),                  // as in the Ibex adapter (fair area comparison)
+      .RV32M         (cve2_pkg::RV32MFast),
+      .XInterface    (1'b0)
+  ) u_core (
+      .clk_i              (clk_i),
+      .rst_ni             (rst_ni),
+      .test_en_i          (1'b0),
+      .ram_cfg_i          ('0),
+
+      .hart_id_i          (32'h0),
+      .boot_addr_i        (BOOT_ADDR),
+
+      .instr_req_o        (instr_req_o),
+      .instr_gnt_i        (instr_gnt_i),
+      .instr_rvalid_i     (instr_rvalid_i),
+      .instr_addr_o       (instr_addr_o),
+      .instr_rdata_i      (instr_rdata_i),
+      .instr_err_i        (1'b0),
+
+      .data_req_o         (data_req_o),
+      .data_gnt_i         (data_gnt_i),
+      .data_rvalid_i      (data_rvalid_i),
+      .data_we_o          (data_we_o),
+      .data_be_o          (data_be_o),
+      .data_addr_o        (data_addr_o),
+      .data_wdata_o       (data_wdata_o),
+      .data_rdata_i       (data_rdata_i),
+      .data_err_i         (1'b0),
+
+      .x_issue_valid_o    (),
+      .x_issue_ready_i    (1'b0),
+      .x_issue_req_o      (),
+      .x_issue_resp_i     ('0),
+      .x_register_o       (),
+      .x_commit_valid_o   (),
+      .x_commit_o         (),
+      .x_result_valid_i   (1'b0),
+      .x_result_ready_o   (),
+      .x_result_i         ('0),
+
+      .irq_software_i     (irq_i[3]),
+      .irq_timer_i        (irq_i[7]),
+      .irq_external_i     (irq_i[11]),
+      .irq_fast_i         (irq_i[31:16]),
+      .irq_nm_i           (1'b0),
+
+      .debug_req_i        (debug_req_i),
+      .debug_halted_o     (),
+      .dm_halt_addr_i     (32'h0),     // no debug module yet
+      .dm_exception_addr_i(32'h0),
+      .crash_dump_o       (),
+
+      .fetch_enable_i     (fetch_enable_i),
+      .core_sleep_o       (core_sleep_o)
+  );
+
+endmodule
diff --git a/rtl/cores/ibex/README.md b/rtl/cores/ibex/README.md
new file mode 100644
index 0000000..be86c61
--- /dev/null
+++ b/rtl/cores/ibex/README.md
@@ -0,0 +1,28 @@
+# ibex — lowRISC Ibex as a reference core
+
+`third_party/ibex` (submodule, pinned commit), wrapped by `rabbit_cpu.sv` so
+the SoC, the firmware and the scripts treat it exactly like the other cores.
+Used for comparison (`../README.md`), not developed here.
+
+Configuration: lowRISC's "small" Ibex — RV32IMC + Zicsr, 2 stages, fast
+multiplier (MUL 3, MULH 4, DIV 37 cycles), flip-flop register file; no
+writeback stage, branch-target ALU, icache, PMP, security features, CHERIoT;
+of the Zc extensions only Zca (= C).
+
+Deviations from the `rabbit_cpu` contract (all documented in the adapter):
+- first fetch at `{boot_addr[31:8], 8'h80}`, vectored `mtvec` at
+  `boot_addr[31:8]` → `boot_addr_i = MTVEC_ADDR`, BOOT_ADDR must be MTVEC_ADDR + 0x80;
+- 15 fast interrupt lines (16..30), the **lowest** line wins
+  (`CORE_CFLAGS := -DIRQ_FAST_LOW_LINE_FIRST`, the irq test expects it);
+- no `irq_ack_o` / `irq_id_o` (tied to 0).
+
+`files.f` was generated from Ibex's FuseSoC core files; after bumping the
+submodule regenerate it as described in `tools/fusesoc_to_filelist.py`.
+For synthesis, `tools/synth_sky130.sh` works around one construct in
+`ibex_top.sv` that Yosys' slang frontend does not elaborate (a lint-only
+signal); the vendor file is not changed.
+
+```bash
+make soc-sim CORE=ibex PROG=muldiv
+tools/synth_sky130.sh ibex
+```
diff --git a/rtl/cores/ibex/core.mk b/rtl/cores/ibex/core.mk
new file mode 100644
index 0000000..f0168a9
--- /dev/null
+++ b/rtl/cores/ibex/core.mk
@@ -0,0 +1,9 @@
+# Per-core build settings, included by the top-level and dv Makefiles.
+CORE_MARCH       := rv32imc_zicsr
+CORE_MABI        := ilp32
+# Vendor code: keep warnings non-fatal; Ibex' own Verilator waivers are not used.
+CORE_VERILATOR_FLAGS := -Wno-fatal
+# Contract deviation: among the fast interrupt lines the LOWEST line wins
+# (CV32E40P and the rabbit cores: the highest). Ibex has 15 fast lines
+# (16..30); line 31 does not exist.
+CORE_CFLAGS      := -DIRQ_FAST_LOW_LINE_FIRST
diff --git a/rtl/cores/ibex/files.f b/rtl/cores/ibex/files.f
new file mode 100644
index 0000000..389517f
--- /dev/null
+++ b/rtl/cores/ibex/files.f
@@ -0,0 +1,147 @@
+// lowRISC Ibex (third_party/ibex, pinned commit) + rabbit_cpu adapter. ${REPO} is expanded by make.
+// Generated from Ibex's FuseSoC core files (lowrisc:ibex:ibex_top, lint target) with
+// tools/fusesoc_to_filelist.py; regenerate after bumping the submodule (see that script).
++incdir+${REPO}/third_party/ibex/vendor/lowrisc_ip/dv/sv/dv_utils
++incdir+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl
+${REPO}/third_party/ibex/rtl/ibex_pkg.sv
+${REPO}/third_party/ibex/rtl/ibex_cheriot_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_1p_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_2p_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_rom_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_1r1w_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_cipher_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_and2.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_buf.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_clock_buf.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_clock_gating.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_flop.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_flop_no_rst.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_usb_diff_rx.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_xnor2.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_xor2.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_pad_wrapper_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_22_16_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_22_16_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_28_22_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_28_22_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_39_32_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_39_32_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_64_57_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_64_57_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_72_64_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_72_64_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_22_16_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_22_16_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_39_32_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_39_32_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_72_64_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_72_64_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_76_68_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_hamming_76_68_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_22_16_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_22_16_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_28_22_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_28_22_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_39_32_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_39_32_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_64_57_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_64_57_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_72_64_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_72_64_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_22_16_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_22_16_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_39_32_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_39_32_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_72_64_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_72_64_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_76_68_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_inv_hamming_76_68_enc.sv
+${REPO}/third_party/ibex/rtl/ibex_icache.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_cdc_rand_delay.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_subst_perm.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_present.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_prince.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_count_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_count.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_clock_mux2.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_pad_attr.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_pad_wrapper.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_1p.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_1r1w.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_ram_2p.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_rom.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_lfsr.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi_pkg.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_sec_anchor_buf.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_sec_anchor_flop.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_util_pkg.sv
+${REPO}/third_party/ibex/vendor/pulp_common_cells/rtl/stream_fork.sv
+${REPO}/third_party/ibex/vendor/pulp_common_cells/rtl/stream_join_dynamic.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_clock_inv.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_flop_2sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_flop_en.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi4_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi4_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi4_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi8_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi8_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi8_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi12_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi12_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi12_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi16_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi16_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi16_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi20_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi20_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi20_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi24_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi24_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi24_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi28_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi28_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi28_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi32_sender.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi32_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_mubi32_dec.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_onehot_enc.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_onehot_mux.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_adv.sv
+${REPO}/third_party/ibex/rtl/ibex_cheriot_ex.sv
+${REPO}/third_party/ibex/rtl/ibex_alu.sv
+${REPO}/third_party/ibex/rtl/ibex_branch_predict.sv
+${REPO}/third_party/ibex/rtl/ibex_compressed_decoder.sv
+${REPO}/third_party/ibex/rtl/ibex_controller.sv
+${REPO}/third_party/ibex/rtl/ibex_cs_registers.sv
+${REPO}/third_party/ibex/rtl/ibex_csr.sv
+${REPO}/third_party/ibex/rtl/ibex_counter.sv
+${REPO}/third_party/ibex/rtl/ibex_decoder.sv
+${REPO}/third_party/ibex/rtl/ibex_ex_block.sv
+${REPO}/third_party/ibex/rtl/ibex_fetch_fifo.sv
+${REPO}/third_party/ibex/rtl/ibex_id_stage.sv
+${REPO}/third_party/ibex/rtl/ibex_if_stage.sv
+${REPO}/third_party/ibex/rtl/ibex_load_store_unit.sv
+${REPO}/third_party/ibex/rtl/ibex_multdiv_fast.sv
+${REPO}/third_party/ibex/rtl/ibex_multdiv_slow.sv
+${REPO}/third_party/ibex/rtl/ibex_prefetch_buffer.sv
+${REPO}/third_party/ibex/rtl/ibex_pmp.sv
+${REPO}/third_party/ibex/rtl/ibex_wb_stage.sv
+${REPO}/third_party/ibex/rtl/ibex_dummy_instr.sv
+${REPO}/third_party/ibex/rtl/ibex_core.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_fifo_async_sram_adapter.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_fifo_async_simple.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_fifo_async.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_fifo_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_fifo_sync_cnt.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_clock_div.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_rst_sync.sv
+${REPO}/third_party/ibex/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_scr.sv
+${REPO}/third_party/ibex/rtl/ibex_register_file_ff.sv
+${REPO}/third_party/ibex/rtl/ibex_register_file_fpga.sv
+${REPO}/third_party/ibex/rtl/ibex_register_file_latch.sv
+${REPO}/third_party/ibex/rtl/ibex_trvk.sv
+${REPO}/third_party/ibex/rtl/ibex_lockstep.sv
+${REPO}/third_party/ibex/rtl/ibex_top.sv
+${REPO}/rtl/cores/ibex/rabbit_cpu.sv
diff --git a/rtl/cores/ibex/rabbit_cpu.sv b/rtl/cores/ibex/rabbit_cpu.sv
new file mode 100644
index 0000000..5a9ba11
--- /dev/null
+++ b/rtl/cores/ibex/rabbit_cpu.sv
@@ -0,0 +1,150 @@
+// rabbit_cpu adapter for lowRISC Ibex (third_party/ibex, pinned commit).
+// Configuration: "small" Ibex as documented by lowRISC - RV32IMC + Zicsr,
+// 2-stage, fast multiplier (RV32MFast), flip-flop register file, no
+// writeback stage, no branch target ALU, no icache, no PMP, no security
+// features (SecureIbex = 0), CHERIoT off, only Zca of the Zc extensions.
+// See rtl/cores/README.md for the port contract.
+//
+// Differences from the contract (documented, not hidden):
+// - Ibex fetches its first instruction at {boot_addr[31:8], 8'h80} and puts
+//   the vectored mtvec at boot_addr[31:8]: so boot_addr_i = MTVEC_ADDR, and
+//   BOOT_ADDR must be MTVEC_ADDR + 0x80 (the contract defaults are).
+// - 15 fast interrupt lines (16..30); line 31 is ignored. Among them the
+//   lowest line has the highest priority.
+// - irq_ack_o / irq_id_o do not exist on Ibex: tied to 0.
+module rabbit_cpu
+  import ibex_pkg::*;
+#(
+    parameter logic [31:0] BOOT_ADDR  = 32'h0000_0080,
+    parameter logic [31:0] MTVEC_ADDR = 32'h0000_0000
+) (
+    input  logic        clk_i,
+    input  logic        rst_ni,
+    input  logic        fetch_enable_i,
+
+    output logic        instr_req_o,
+    input  logic        instr_gnt_i,
+    input  logic        instr_rvalid_i,
+    output logic [31:0] instr_addr_o,
+    input  logic [31:0] instr_rdata_i,
+
+    output logic        data_req_o,
+    input  logic        data_gnt_i,
+    input  logic        data_rvalid_i,
+    output logic        data_we_o,
+    output logic [ 3:0] data_be_o,
+    output logic [31:0] data_addr_o,
+    output logic [31:0] data_wdata_o,
+    input  logic [31:0] data_rdata_i,
+
+    input  logic [31:0] irq_i,
+    output logic        irq_ack_o,
+    output logic [ 4:0] irq_id_o,
+
+    input  logic        debug_req_i,
+    output logic        core_sleep_o
+);
+
+  if (MTVEC_ADDR[7:0] != 8'h00 || BOOT_ADDR != MTVEC_ADDR + 32'h80) begin : g_bad_addr
+    $error("ibex adapter: needs MTVEC_ADDR 256-byte aligned and BOOT_ADDR = MTVEC_ADDR + 0x80");
+  end
+
+  assign irq_ack_o = 1'b0;
+  assign irq_id_o  = '0;
+
+  logic unused_irq31;
+  assign unused_irq31 = irq_i[31];
+
+  ibex_top #(
+      .RV32M          (RV32MFast),
+      .RV32B          (RV32BNone),
+      .RV32ZC         (RV32Zca),
+      .RegFile        (RegFileFF),
+      .BranchTargetALU(1'b0),
+      .WritebackStage (1'b0),
+      .ICache         (1'b0),
+      .BranchPredictor(1'b0),
+      .DbgTriggerEn   (1'b0),
+      .SecureIbex     (1'b0),
+      .PMPEnable      (1'b0),
+      .MHPMCounterNum (0)
+  ) u_core (
+      .clk_i                  (clk_i),
+      .rst_ni                 (rst_ni),
+      .test_en_i              (1'b0),
+      .ram_cfg_icache_tag_i   ('0),
+      .ram_cfg_icache_tag_o   (),
+      .ram_cfg_icache_data_i  ('0),
+      .ram_cfg_icache_data_o  (),
+      .cheriot_enable_i       (IbexMuBiOff),
+
+      .hart_id_i              (32'h0),
+      .boot_addr_i            (MTVEC_ADDR),
+      .trvk_heap_base_addr_i  (32'h0),
+
+      .instr_req_o            (instr_req_o),
+      .instr_gnt_i            (instr_gnt_i),
+      .instr_rvalid_i         (instr_rvalid_i),
+      .instr_addr_o           (instr_addr_o),
+      .instr_rdata_i          (instr_rdata_i),
+      .instr_rdata_intg_i     ('0),
+      .instr_err_i            (1'b0),
+
+      .data_req_o             (data_req_o),
+      .data_gnt_i             (data_gnt_i),
+      .data_rvalid_i          (data_rvalid_i),
+      .data_we_o              (data_we_o),
+      .data_be_o              (data_be_o),
+      .data_addr_o            (data_addr_o),
+      .data_wdata_o           (data_wdata_o),
+      .data_wdata_intg_o      (),
+      .data_tag_o             (),
+      .data_rdata_i           (data_rdata_i),
+      .data_rdata_intg_i      ('0),
+      .data_tag_i             (1'b0),
+      .data_err_i             (1'b0),
+
+      .trvk_revbm_req_o       (),
+      .trvk_revbm_gnt_i       (1'b0),
+      .trvk_revbm_rvalid_i    (1'b0),
+      .trvk_revbm_addr_o      (),
+      .trvk_revbm_rdata_i     ('0),
+      .trvk_revbm_rdata_intg_i('0),
+      .trvk_revbm_err_i       (1'b0),
+
+      .irq_software_i         (irq_i[3]),
+      .irq_timer_i            (irq_i[7]),
+      .irq_external_i         (irq_i[11]),
+      .irq_fast_i             (irq_i[30:16]),
+      .irq_nm_i               (1'b0),
+
+      .scramble_key_valid_i   (1'b0),
+      .scramble_key_i         ('0),
+      .scramble_nonce_i       ('0),
+      .scramble_req_o         (),
+
+      .debug_req_i            (debug_req_i),
+      .crash_dump_o           (),
+      .double_fault_seen_o    (),
+
+      .fetch_enable_i         (fetch_enable_i ? IbexMuBiOn : IbexMuBiOff),
+      .mcounteren_writable_i  (IbexMuBiOn),
+      .alert_minor_o          (),
+      .alert_major_internal_o (),
+      .alert_major_bus_o      (),
+      .core_sleep_o           (core_sleep_o),
+
+      // lockstep / scan test (SecureIbex = 0: unused)
+      .scan_rst_ni            (1'b1),
+      .lockstep_cmp_en_o      (),
+      .data_req_shadow_o      (),
+      .data_we_shadow_o       (),
+      .data_be_shadow_o       (),
+      .data_addr_shadow_o     (),
+      .data_wdata_shadow_o    (),
+      .data_wdata_intg_shadow_o(),
+      .instr_req_shadow_o     (),
+      .instr_addr_shadow_o    ()
+  );
+
+endmodule
diff --git a/rtl/cores/rabbit3/README.md b/rtl/cores/rabbit3/README.md
index 79c061b..f979a56 100644
--- a/rtl/cores/rabbit3/README.md
+++ b/rtl/cores/rabbit3/README.md
@@ -27,8 +27,8 @@ F ──► X ──────────────────────
 Then run both and look at the difference:
 
 ```bash
-make soc-sim   CORE=rabbit3            # hello: 2756 cycles
-make soc-sim   CORE=rabbit5            # hello: 3471 cycles
+make soc-sim   CORE=rabbit3            # hello: 2758 cycles
+make soc-sim   CORE=rabbit5            # hello: 3473 cycles
 make soc-sim   CORE=rabbit3 PROG=irq   # interrupt self-test (also rabbit5, cv32e40p)
 make soc-sim   CORE=rabbit3 PROG=muldiv  # M extension self-test + timing
 make soc-waves CORE=rabbit3            # waveform: dv/cocotb/soc/dump.fst
@@ -49,7 +49,7 @@ make gls-smoke CORE=rabbit3            # same firmware on the gate netlist
 | WFI sleep (`core_sleep_o` for clock gating) | yes, fetch restarts in the cycle the interrupt appears | same |
 | MUL, MULH, MULHSU, MULHU (R8) | **2 cycles** (1 extra), any operands | same |
 | DIV, DIVU, REM, REMU (R8) | **34 cycles** (33 extra), any operands; an interrupt abandons it | same |
-| `hello` (RV32IM) | 2756 cycles (RV32I: 3145) | 3471 cycles (RV32I: 3958) |
+| `hello` (RV32IM) | 2758 cycles (RV32I: 3145) | 3473 cycles (RV32I: 3958) |
 | Size, sky130 (`synth -booth`, incl. adapter) | 114.9 k µm² (RV32I: 81.1 k) | 126.5 k µm² (RV32I: 95.4 k) |
 | Longest combinational path (qualitative) | memory → load align → register bypass → ALU → data address | one stage of that |
 
diff --git a/rtl/cores/rabbit5/README.md b/rtl/cores/rabbit5/README.md
index 357533a..0c01843 100644
--- a/rtl/cores/rabbit5/README.md
+++ b/rtl/cores/rabbit5/README.md
@@ -17,14 +17,14 @@ IF ──► ID ──► EX ──► MEM ──► WB
 
 | What | Result | Command |
 |---|---|---|
-| `hello` firmware in the SoC | PASS, 3471 cycles (RV32I: 3958; rabbit3: 2756, CV32E40P: 3450) | `make soc-sim CORE=rabbit5` |
+| `hello` firmware in the SoC | PASS, 3473 cycles (RV32I: 3958; rabbit3: 2758, CV32E40P: 3447) | `make soc-sim CORE=rabbit5` |
 | riscv-formal (45 instructions incl. M with ALTOPS + reg, pc_fwd, pc_bwd, causal, unique, liveness, ill, cover) | **53/53 PASS** | `make formal CORE=rabbit5` |
 | M extension: multiply 2 cycles, divide 34, for any operands (R8, T1); unit proof of the arithmetic | PASS | `make formal CORE=rabbit5` |
 | M self-test firmware (corner cases, random, timing, interrupt during divide) | PASS (same test on CV32E40P / rabbit3) | `make soc-sim CORE=rabbit5 PROG=muldiv` |
 | Timing properties T1–T4 (ours, beyond riscv-formal) | PASS (BMC depth 24) + all covers reached | `make formal CORE=rabbit5` |
 | Interrupts + WFI: properties I1–I4, W0–W2; latency ≤ **7 cycles** (tight) | PASS + all covers reached | `make formal CORE=rabbit5` |
 | Interrupt self-test firmware (same as on CV32E40P / rabbit3) | PASS, 9025 cycles | `make soc-sim CORE=rabbit5 PROG=irq` |
-| Gate-level smoke test (Yosys generic gates) | PASS, **same cycles** as RTL (hello 3471, irq 9025, muldiv) | `make gls-smoke CORE=rabbit5` |
+| Gate-level smoke test (Yosys generic gates) | PASS, **same cycles** as RTL (hello 3473, irq 9025, muldiv) | `make gls-smoke CORE=rabbit5` |
 | Verilator `-Wall` lint | clean | `make lint CORE=rabbit5` |
 | Size, sky130 (`synth -booth` + ABC, core + adapter) | 126.5 k µm² (RV32I: 95.4 k; CV32E40P: 170.3 k) | see `../rabbit_common/README.md` |
 
diff --git a/rtl/cores/rabbit_common/README.md b/rtl/cores/rabbit_common/README.md
index e0ecba6..fce4716 100644
--- a/rtl/cores/rabbit_common/README.md
+++ b/rtl/cores/rabbit_common/README.md
@@ -35,7 +35,8 @@ Everything an instruction *does* lives here. A rabbit core
 Rules for this directory:
 - nothing here may know how many stages a core has;
 - a change here affects every core → run `make formal CORE=rabbit3` **and**
-  `make formal CORE=rabbit5` (CI does both).
+  `make formal CORE=rabbit5` (or `tools/check_all.sh formal`; on GitHub: the
+  on-demand `deep-verify` workflow).
 
 ## M extension (`rabbit_muldiv.sv`)
 
@@ -78,10 +79,14 @@ Whole cores (core + adapter):
 | Core | Area µm² | Longest path | `hello` cycles |
 |---|---|---|---|
 | rabbit3 RV32I | 81 064 | 10.0 ns | 3145 |
-| **rabbit3 RV32IM** | **114 853** (+42 %) | 10.0–10.7 ns | **2756** |
+| **rabbit3 RV32IM** | **114 853** (+42 %) | 10.0–10.7 ns | **2758** |
 | rabbit5 RV32I | 95 381 | 9.2 ns | 3958 |
-| **rabbit5 RV32IM** | **126 549** (+33 %) | 9.0–9.5 ns | **3471** |
-| CV32E40P RV32IMC (reference) | 170 298 | 6.9 ns | 3450 |
+| **rabbit5 RV32IM** | **126 549** (+33 %) | 9.0–9.5 ns | **3473** |
+| CV32E40P RV32IMC (reference) | 170 298 | 6.9 ns | 3447 |
+| Ibex "small" RV32IMC (reference) | 124 899 | 6.4 ns | 3984 |
+| CVE2 RV32IMC (reference) | 128 964 | 6.5 ns | 3984 |
+
+Full comparison (also M and interrupt timing): `../README.md`.
 
 - The longest path does not go through the M unit: in every run it is
   instruction word → decode / trap logic → enable of the 64-bit `minstret` /
diff --git a/sw/baremetal/Makefile b/sw/baremetal/Makefile
index a0bc395..cebe1e5 100644
--- a/sw/baremetal/Makefile
+++ b/sw/baremetal/Makefile
@@ -15,7 +15,8 @@ OBJDUMP= $(CROSS)objdump
 COMMON = $(REPO)/sw/baremetal/common
 OUT    = build/$(CORE)/$(PROG)
 
-CFLAGS  = -march=$(CORE_MARCH) -mabi=$(CORE_MABI) -O2 -g -Wall -Wextra \
+# 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 \
           -ffreestanding -fno-builtin -nostdlib -I$(COMMON)
 LDFLAGS = -T $(COMMON)/link.ld -nostartfiles -nostdlib -Wl,--gc-sections -Wl,--no-warn-rwx-segments -lgcc
 
@@ -23,7 +24,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
+$(OUT)/$(PROG).elf: $(SRCS) $(COMMON)/link.ld $(COMMON)/rabbit_sim.h $(REPO)/rtl/cores/$(CORE)/core.mk
 	@mkdir -p $(OUT)
 	$(CC) $(CFLAGS) $(SRCS) -o $@ $(LDFLAGS)
 
diff --git a/sw/baremetal/hello/main.c b/sw/baremetal/hello/main.c
index 4eba067..dc9710e 100644
--- a/sw/baremetal/hello/main.c
+++ b/sw/baremetal/hello/main.c
@@ -32,10 +32,10 @@ int main(void) {
     check("divs   ", (uint32_t)((int32_t)neg / 7), (uint32_t)-11);
     check("fib(30)", fib(30), 832040u);
 
-    uint32_t t0 = csr_mcycle();
+    uint32_t t0 = sim_cycles();     /* SoC counter: CV32E40P resets with mcycle stopped */
     volatile uint32_t acc = 0;
     for (int i = 0; i < 100; i++) acc += i;
-    uint32_t t1 = csr_mcycle();
+    uint32_t t1 = sim_cycles();
     check("sum0_99", acc, 4950u);
     sim_puts("  loop cycles = "); sim_puthex(t1 - t0); sim_putc('\n');
 
diff --git a/sw/baremetal/irq/main.c b/sw/baremetal/irq/main.c
index 2ec38df..9a052f9 100644
--- a/sw/baremetal/irq/main.c
+++ b/sw/baremetal/irq/main.c
@@ -4,6 +4,8 @@
  *   1. mip shows the request lines, and only the lines that exist
  *   2. mstatus.MIE = 0 holds an interrupt back; setting it takes the interrupt
  *   3. priority: several lines at once are handled 17 > 16 > 11 > 7
+ *      (cores whose core.mk defines IRQ_FAST_LOW_LINE_FIRST, e.g. Ibex/CVE2:
+ *      16 > 17 > 11 > 7)
  *   4. a periodic timer "control loop" with WFI between ticks; lateness
  *   5. WFI with interrupts globally off: wakes up, but no handler runs
  *   6. latency from raising a line to the first handler instruction (printed)
@@ -101,8 +103,13 @@ int main(void) {
     irq_global_enable();
     spin(5);
     check("priority count   ", n_irq, 4);
+#ifdef IRQ_FAST_LOW_LINE_FIRST
+    check("  1st (fast 0)   ", order[0], IRQ_FAST(0));
+    check("  2nd (fast 1)   ", order[1], IRQ_FAST(1));
+#else
     check("  1st (fast 1)   ", order[0], IRQ_FAST(1));
     check("  2nd (fast 0)   ", order[1], IRQ_FAST(0));
+#endif
     check("  3rd (MEI)      ", order[2], IRQ_MEI);
     check("  4th (MTI)      ", order[3], IRQ_MTI);
 
diff --git a/sw/baremetal/muldiv/main.c b/sw/baremetal/muldiv/main.c
index 7bfebe1..4d48d5b 100644
--- a/sw/baremetal/muldiv/main.c
+++ b/sw/baremetal/muldiv/main.c
@@ -108,12 +108,15 @@ 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"};
 
-/* ---- timing: cycles from one mcycle read to the next, around one instruction */
+/* ---- 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). */
 #define TIMED(insn) \
     static uint32_t time_##insn(uint32_t a, uint32_t b) { \
         uint32_t t0, t1, r; \
-        __asm__ volatile("csrr %0, mcycle\n\t" #insn " %2, %3, %4\n\tcsrr %1, mcycle" \
-                         : "=&r"(t0), "=&r"(t1), "=&r"(r) : "r"(a), "r"(b)); \
+        __asm__ volatile("lw %0, 0(%3)\n\t" #insn " %2, %4, %5\n\tlw %1, 0(%3)" \
+                         : "=&r"(t0), "=&r"(t1), "=&r"(r) \
+                         : "r"(RABBIT_SIM_CYCLE), "r"(a), "r"(b)); \
         (void)r; return t1 - t0; }
 TIMED(add) TIMED(mul) TIMED(mulhu) TIMED(div) TIMED(remu)
 
diff --git a/third_party/cve2 b/third_party/cve2
new file mode 160000
index 0000000..d7f2156
--- /dev/null
+++ b/third_party/cve2
@@ -0,0 +1 @@
+Subproject commit d7f21568028a1114be663599bd42145dccf28928
diff --git a/third_party/ibex b/third_party/ibex
new file mode 160000
index 0000000..626034d
--- /dev/null
+++ b/third_party/ibex
@@ -0,0 +1 @@
+Subproject commit 626034d7557ab85a6d989b13011b44296bad26fa
diff --git a/tools/check_all.sh b/tools/check_all.sh
index d3a2847..d17486b 100755
--- a/tools/check_all.sh
+++ b/tools/check_all.sh
@@ -2,7 +2,7 @@
 # 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 cores, muldiv exhaustive sim  (~1 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 synth           sky130 area / delay table (needs the sky130 PDK)     (~1 min)
@@ -51,7 +51,7 @@ for stage in $STAGES; do
   echo "=== $stage"
   case $stage in
     quick)
-      for c in rabbit3 rabbit5 cv32e40p; do
+      for c in rabbit3 rabbit5 cv32e40p cve2 ibex; do
         step "quick/lint-$c" "" make lint CORE=$c
         for p in hello irq muldiv; do
           step "quick/sim-$c-$p" "RESULT: PASS" make soc-sim CORE=$c PROG=$p
diff --git a/tools/fusesoc_to_filelist.py b/tools/fusesoc_to_filelist.py
new file mode 100755
index 0000000..9f628d8
--- /dev/null
+++ b/tools/fusesoc_to_filelist.py
@@ -0,0 +1,51 @@
+#!/usr/bin/env python3
+"""Turn a FuseSoC/Verilator .vc file list into a rabbit files.f.
+
+FuseSoC copies every file into its build directory (src/<core>/...). This maps
+each entry back to the original file inside the given source tree, so the
+files.f works without FuseSoC. Used for rtl/cores/ibex/files.f:
+
+  uv run --with fusesoc fusesoc --cores-root third_party/ibex \\
+      run --target=lint --setup --build-root /tmp/fsoc lowrisc:ibex:ibex_top
+  tools/fusesoc_to_filelist.py /tmp/fsoc/.../lowrisc_ibex_ibex_top_0.1.vc \\
+      third_party/ibex > rtl/cores/ibex/files.part.f
+"""
+import sys
+from pathlib import Path
+
+vc, tree = Path(sys.argv[1]), Path(sys.argv[2]).resolve()
+repo = Path(__file__).resolve().parent.parent
+
+# FuseSoC names each build sub-directory after the core: "lowrisc:prim:util:0.1"
+# becomes src/lowrisc_prim_util_0.1. Map those names to the .core file's folder.
+core_dir = {}
+for core in tree.rglob("*.core"):
+    for line in core.read_text(errors="ignore").splitlines():
+        if line.startswith("name:"):
+            name = line.split(":", 1)[1].strip().strip('"').strip("'")
+            vlnv = name.split(":")
+            if len(vlnv) == 3:
+                vlnv.append("0")                   # FuseSoC's default version
+            core_dir["_".join(vlnv)] = core.parent
+            break
+
+
+def original(rel):
+    parts = Path(rel).parts
+    if parts[0] not in core_dir:
+        sys.exit(f"unknown core directory {parts[0]} (in {rel})")
+    return core_dir[parts[0]].joinpath(*parts[1:])
+
+
+out = []
+for line in vc.read_text().split("\n"):
+    line = line.strip()
+    if line.startswith("+incdir+src/"):
+        d = original(line[len("+incdir+src/"):])
+        out.append("+incdir+${REPO}/" + d.relative_to(repo).as_posix())
+    elif line.startswith("src/") and line.endswith((".sv", ".svh", ".v")):
+        f = original(line[len("src/"):])
+        if not f.is_file():
+            sys.exit(f"missing {f}")
+        out.append("${REPO}/" + f.relative_to(repo).as_posix())
+print("\n".join(out))
diff --git a/tools/synth_sky130.sh b/tools/synth_sky130.sh
index 2bdd562..40ee3ba 100755
--- a/tools/synth_sky130.sh
+++ b/tools/synth_sky130.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 # Area and longest combinational path of the cores on sky130 (Yosys + ABC).
 #
-#   tools/synth_sky130.sh                 rabbit3 rabbit5 cv32e40p
+#   tools/synth_sky130.sh                 rabbit3 rabbit5 cv32e40p cve2 ibex
 #   tools/synth_sky130.sh rabbit3         one core
 #
 # Finds the sky130_fd_sc_hd typical-corner liberty file in $SKY130_LIB, or
@@ -28,12 +28,20 @@ fi
 
 OUT=build/synth_sky130
 mkdir -p "$OUT"
-CORES=${*:-rabbit3 rabbit5 cv32e40p}
+CORES=${*:-rabbit3 rabbit5 cv32e40p cve2 ibex}
 
 printf '%-10s %14s %12s %12s\n' core "area um2" "of it flops" "delay ns"
 for c in $CORES; do
   # files.f: drop comments, expand ${REPO}, turn +incdir+ into -I
   SRC=$(grep -v '^//' "rtl/cores/$c/files.f" | sed "s|\${REPO}|$REPO|" | sed 's|^+incdir+|-I |' | tr '\n' ' ')
+  if [ "$c" = ibex ]; then
+    # slang cannot elaborate a module-level variable whose initializer reads
+    # nets (ibex_top.sv, a lint-only "unused" signal). Synthesize a copy where
+    # it is a plain assign; the vendor file itself is not touched.
+    sed 's/logic unused_scramble_inputs = /logic unused_scramble_inputs; assign unused_scramble_inputs = /' \
+        third_party/ibex/rtl/ibex_top.sv > "$OUT/ibex_top.sv"
+    SRC=${SRC//$REPO\/third_party\/ibex\/rtl\/ibex_top.sv/$REPO/$OUT/ibex_top.sv}
+  fi
   yosys -p "read_slang $SRC --top rabbit_cpu -DSYNTHESIS; \
             synth -top rabbit_cpu -booth -flatten; \
             dfflibmap -liberty $LIB; \