abmajith · Nov 7, 2026 · Nov 7, 2026 · Nov 7, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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