Rabbit mext

.github/workflows/ci.yml

@@ -36,7 +36,7 @@ jobs:
       matrix:
         core: [cv32e40p, rabbit3, rabbit5]
         # irq: interrupt self-test; cv32e40p is the reference the rabbits must match
-        prog: [hello, irq]
+        prog: [hello, irq, muldiv]
     steps:
       - name: RISC-V GCC
         run: apt-get update -q && apt-get install -y -q gcc-riscv64-unknown-elf libpython3.12-dev
@@ -69,7 +69,8 @@ jobs:
       - working-directory: hw_ip/sim
         run: uv run make TARGET=${{ matrix.target }}   # non-zero exit on any failed test
 
-  # riscv-formal (45 checks) + timing properties, for each of our own cores.
+  # 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
@@ -133,6 +134,9 @@ jobs:
         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
 
   rma-smoke:
     runs-on: ubuntu-24.04

.gitignore

@@ -39,3 +39,7 @@ build/
 dv/formal/rabbit/build/
 dv/formal/rabbit/*.log
 dv/formal/rabbit/timing/timing*/
+
+# SymbiYosys work directories of the muldiv unit proof
+dv/formal/rabbit/muldiv/muldiv/
+dv/formal/rabbit/muldiv/muldiv_*/

Makefile

@@ -8,6 +8,7 @@
 #   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 check-all      reproduce all rabbit checks (STAGES="quick gls formal synth mutants")
 REPO := $(abspath .)
 export REPO
 CORE ?= cv32e40p
@@ -72,7 +73,9 @@ formal:
 GLS_DIR := build/gls/$(CORE)
 YOSYS_SLANG := $(shell yosys -p 'help read_slang' >/dev/null 2>&1 || echo -m slang)
 gls-netlist: $(GLS_DIR)/rabbit_cpu_netlist.v
-$(GLS_DIR)/rabbit_cpu_netlist.v: $(wildcard rtl/cores/$(CORE)/*.sv)
+# 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
 	@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' ' ') \
@@ -86,10 +89,15 @@ gls-smoke: sync gls-netlist
 
 ci: lint soc-sim ip-test rma-smoke
 
+# Reproduce everything (see tools/check_all.sh; default stages: quick gls)
+STAGES ?=
+check-all:
+	tools/check_all.sh $(STAGES)
+
 clean:
 	$(MAKE) -C sw/baremetal clean
 	cd dv/cocotb/soc && rm -rf sim_build_* results.xml dump.fst
 	rm -rf build dv/formal/rabbit/build
 	cd hw_ip/sim && uv run $(MAKE) clean
 
-.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke formal gls-netlist gls-smoke ci clean
+.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke formal gls-netlist gls-smoke ci check-all clean

README.md

@@ -5,7 +5,7 @@ FPGA → open-source ASIC, evaluated with Zephyr and real-time Linux, with a
 vector / quantized-NN block. Five-year plan and research notes are kept
 outside the repository.
 
-CPUs: **rabbit5**, our own timing-predictable 5-stage RV32I core
+CPUs: **rabbit3** / **rabbit5**, our own timing-predictable 3- and 5-stage RV32IM cores
 ([`rtl/cores/rabbit5/README.md`](rtl/cores/rabbit5/README.md)), and **OpenHW
 CV32E40P** (RV32IMC) as reference. Every layer above the CPU talks to a
 core-agnostic `rabbit_cpu` contract, so cores plug in the same way:
@@ -17,12 +17,29 @@ core-agnostic `rabbit_cpu` contract, so cores plug in the same way:
 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
-make formal                  # riscv-formal + timing properties for rabbit5 (~35 s)
+make soc-sim CORE=rabbit5    # ... on our own core (also rabbit3; PROG=irq, PROG=muldiv)
+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
 ```
 
+### Reproduce every result
+
+`tools/check_all.sh` (or `make check-all STAGES="..."`) reruns every check
+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 |
+| `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 |
+| `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
+needed: OSS CAD Suite (yosys + slang, sby, boolector, verilator),
+`riscv64-unknown-elf-gcc`, `uv`.
+
 Walkthrough: [`docs/GETTING_STARTED.md`](docs/GETTING_STARTED.md) ·
 Status and known issues: [`docs/STATUS.md`](docs/STATUS.md)
 
@@ -36,7 +53,7 @@ Status and known issues: [`docs/STATUS.md`](docs/STATUS.md)
 | `dv/` | Verification: `cocotb/` (SoC tests), `isa/`, `formal/` |
 | `sw/` | `baremetal/` programs, `zephyr/` port |
 | `fpga/`, `asic/` | FPGA (LiteX) and open-silicon flows |
-| `tools/` | Build helpers; `gls/` fast gate-level verification (GPU) |
+| `tools/` | Build helpers; `check_all.sh`, `synth_sky130.sh`, `mutants.py` (reproduce results); `gls/` fast gate-level verification (GPU) |
 | `rma_analysis/` | Rate-monotonic / MSRP schedulability analysis (`uv run rma_analysis <yaml>`) |
 | `rt_rabbit/zephyr-fw/` | Zephyr control firmware |
 | `third_party/` | Git submodules (CV32E40P) |

docs/STATUS.md

@@ -15,16 +15,19 @@
 
 | Item | rabbit3 (3-stage) | rabbit5 (5-stage) |
 |---|---|---|
-| hello (`make soc-sim CORE=...`) | PASS, 3145 cycles | PASS, 3958 cycles |
+| ISA | RV32IM + Zicsr | RV32IM + Zicsr |
+| hello (`make soc-sim CORE=...`) | PASS, 2756 cycles | PASS, 3471 cycles |
 | interrupts + WFI (`PROG=irq`, same test passes on cv32e40p) | PASS, 7448 cycles | PASS, 9025 cycles |
-| riscv-formal (`make formal CORE=...`) | 45/45 | 45/45 |
+| 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 |
+| multiply/divide unit proof (`make -C dv/formal/rabbit muldiv`) | PASS: values for all inputs at 4/6/8 bits, latency at 32 bits | (shared) |
 | timing properties T1–T4 + covers | PASS | PASS |
 | 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) | PASS, same cycles (hello, irq) |
-| size, Yosys generic gates | 10.4 k cells | 11.5 k cells |
+| 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² |
 
-Next: riscv-formal CSR checks, RISCOF compliance, Zmmul, then the dual-core
-TDM work (M4).
+Next: int8 (and int4) SIMD dot product for quantized inference, riscv-formal
+CSR checks, RISCOF compliance, then the dual-core TDM work (M4).
 Learning path: `rtl/cores/rabbit3/README.md`.
 
 ## Known issues
@@ -48,6 +51,7 @@ Learning path: `rtl/cores/rabbit3/README.md`.
 - [x] CI pipeline
 - [x] Own core rabbit5 v0 with riscv-formal, timing properties, GLS smoke (2026-11-06)
 - [x] Machine timer (mtime/mtimecmp) + interrupt test; rabbit3/rabbit5 interrupts + WFI with proven latency (2026-11-06)
+- [x] M extension on rabbit3/rabbit5: fixed-latency multiply (2) / divide (34), interruptible, proven (2026-11-06)
 - [ ] OBI→Wishbone bridge; attach PWM / QEI / telemetry to the CPU
 - [ ] UART (needed for FPGA and Zephyr console)
 - [ ] RISCOF + riscv-arch-test on CV32E40P (`dv/isa/`)

dv/cocotb/soc/test_soc.py

@@ -10,7 +10,7 @@
 from cocotb.clock import Clock
 from cocotb.triggers import ClockCycles, RisingEdge
 
-MAX_CYCLES = int(os.environ.get("RABBIT_MAX_CYCLES", "200000"))
+MAX_CYCLES = int(os.environ.get("RABBIT_MAX_CYCLES", "1000000"))
 
 
 async def run_firmware(dut, max_cycles: int = MAX_CYCLES):

dv/formal/README.md

@@ -8,14 +8,17 @@ One flow for every rabbit core, selected with `CORE=`:
 make formal CORE=rabbit3                       # from the repo root: everything below
 make -C dv/formal/rabbit CORE=rabbit5 riscv-formal
 make -C dv/formal/rabbit CORE=rabbit5 timing
+make -C dv/formal/rabbit muldiv                               # multiply/divide unit (any core)
 make -C dv/formal/rabbit CORE=rabbit3 check C=insn_add_ch0    # one check
 ```
 
 | Part | What it proves | Files |
 |---|---|---|
-| **riscv-formal** (YosysHQ, submodule) | every RV32I instruction computes what the ISA says (37 checks), plus pipeline consistency: `reg` (forwarding/bypass), `pc_fwd`/`pc_bwd` (branches, flushes), `causal`, `unique`, `liveness`, `ill`, `cover`. The interrupt lines are free inputs, so all of this also holds with interrupts arriving at any time. | `rabbit/checks.cfg` (template), `rabbit/wrapper.sv` |
+| **riscv-formal** (YosysHQ, submodule) | every RV32IM instruction computes what the ISA says (45 checks; MUL/DIV with ALTOPS stand-in results, see below), plus pipeline consistency: `reg` (forwarding/bypass), `pc_fwd`/`pc_bwd` (branches, flushes), `causal`, `unique`, `liveness`, `ill`, `cover`. The interrupt lines are free inputs, so all of this also holds with interrupts arriving at any time. | `rabbit/checks.cfg` (template), `rabbit/wrapper.sv` |
 | **timing properties** (ours) | T1 exact retirement-gap model, T2 first retirement cycle, T3 memory used exactly one cycle before retirement, T4 wake-up from WFI; covers prove every case and the min/max throughput bounds are reachable | `rabbit/timing/rabbit_timing_tb.sv` |
-| **interrupt + sleep properties** (ours, cores with `TIMING_IRQ_LATENCY` > 0) | I1 latency ≤ declared bound, I2 no spurious interrupt, I3 precise `mepc`, I4 correct `mcause`, I5 handler starts at the right vector; W0 sleep only after WFI, W1 wakes on an enabled interrupt, W2 nothing moves while asleep. All 32 interrupt lines free. | same file |
+| **M extension properties** (ours) | T1/T2 include R8 (MUL* exactly +1 cycle, DIV* exactly +DIV_CYCLES−1, whatever the operands); M0 operands do not change while an M instruction waits; M1 (cover) an interrupt is taken while one waits; M2 no instruction fetch while one waits | `rabbit/timing/rabbit_timing_tb.sv` |
+| **multiply/divide unit** (ours) | A1 every result equals the RISC-V definition, L1 exact latency, under any interrupt pattern: every input at W = 4 (unbounded, PDR) and W = 6 (BMC 20), all 524 288 instructions at W = 8 (exhaustive simulation), latency at W = 32 (unbounded) | `rabbit/muldiv/` |
+| **interrupt + sleep properties** (ours, cores with `TIMING_IRQ_LATENCY` > 0) | I1 latency ≤ declared bound (+ the M extra cycles if the handler's first instruction is itself MUL/DIV), I2 no spurious interrupt, I3 precise `mepc`, I4 correct `mcause`, I5 handler starts at the right vector; W0 sleep only after WFI, W1 wakes on an enabled interrupt, W2 nothing moves while asleep. All 32 interrupt lines free. | same file |
 
 Each core **declares** its timing model in `rtl/cores/<core>/core.mk`
 (`TIMING_FIRST_RETIRE`, `TIMING_REDIRECT_GAP`, `TIMING_LOADUSE_GAP`,
@@ -34,8 +37,9 @@ that sleep ends when it must is W1.
 
 | | rabbit3 | rabbit5 |
 |---|---|---|
-| riscv-formal (interrupt lines 7 and 16 free) | 45/45 PASS, ~3 min | 45/45 PASS, ~30 s |
-| timing T1–T4, I1–I5, W0–W2 + 14 covers | PASS, ~15 min | PASS, ~18 min |
+| riscv-formal RV32IM (interrupt lines 7 and 16 free) | 53/53 PASS, ~10 min | 53/53 PASS, ~1 min |
+| timing T1–T4, I1–I5, W0–W2, M0–M2 + covers | PASS, ~35 min | PASS, ~22 min |
+| muldiv unit proof + exhaustive 8-bit simulation (shared) | PASS, ~1 min | (same) |
 | proven worst-case interrupt latency (cover: reached) | 4 cycles | 7 cycles |
 
 riscv-formal gets only two free interrupt lines: with all 32 free, rabbit3's
@@ -59,8 +63,8 @@ How it fits together:
    the converted file made the solver ~60x slower).
 
 Bounded proofs: all results hold for every instruction stream up to the
-configured depth (12–20 cycles for riscv-formal, 24 for timing), not for
-unbounded time.
+configured depth (12–26 cycles for riscv-formal, 24 for timing), not for
+unbounded time (except the muldiv tasks run with PDR, which are unbounded).
 
 ### Mutation results (the checks are not vacuous)
 
@@ -78,6 +82,43 @@ unbounded time.
 | vectored `mtvec` ignored (always jump to the base) | I5 |
 | rabbit5 checked against IRQ_LATENCY=6 | I1 |
 | rabbit5: `stall = load_use` without `&& !redirect` | nothing — an *equivalent* mutant: every user of `stall` already gives `redirect` priority, so the term is redundant |
+| muldiv: x/0 sign rule removed | unit proof A1 (W = 4) + exhaustive simulation |
+| muldiv: MULH ignores the sign of rs2 | unit proof A1 (W = 6) + exhaustive simulation |
+| muldiv: no restart after an interrupt | unit proof L1 + exhaustive simulation |
+| muldiv: divide one cycle longer | unit proof L1 (W = 32) |
+| `rvfi_intr` cleared while an M instruction waits (real bug, fixed) | riscv-formal `pc_fwd` |
+| rabbit5: forwarded operands not stored while EX waits | M0 + riscv-formal `reg` |
+| rabbit3: fetch continues while an M instruction waits | M2 + riscv-formal `pc_fwd` |
+| rabbit3: no instruction holding register while X waits | M0 + riscv-formal `liveness` |
+
+### M extension: how multiply and divide are verified
+
+SAT/SMT solvers cannot prove two different 32-bit multipliers equal (the
+problem blows up beyond ~8 bits: boolector needed > 10 min to reach step 14
+at W = 8). So the work is split:
+
+1. **riscv-formal with ALTOPS** checks everything *around* the arithmetic:
+   decode, operand forwarding, the pipeline holding the instruction, register
+   write-back, interrupts during a wait. With `RISCV_FORMAL_ALTOPS` the core
+   returns stand-in results ((rs1 ± rs2) XOR a constant) with the same timing.
+   The real multiplier is then unused and optimised away, so the proofs stay
+   fast. A divide takes 34 cycles, which does not fit the proof depth, so
+   these proofs use a 2-step divider (`FORMAL_DIV_STEPS`, `core.mk`): the
+   pipeline only ever sees `busy`/`done`, never the step count.
+2. **The unit proof** (`muldiv/`) checks the real arithmetic and the real
+   latency on the very same RTL, which is written for any width W. Exact
+   latency (34 cycles at 32 bits) is a counter property and is proven at full
+   width, for any length of history.
+3. **Simulation**: `sw/baremetal/muldiv` runs corner cases and random 32-bit
+   operands on every core, and checks that the timing does not depend on the
+   data.
+
+Found by this flow while adding M: the "first instruction of the handler"
+flag (`rvfi_intr`) was lost when that instruction was itself a multiply or
+divide (pc_fwd); the liveness window had to grow because an interrupted
+divide followed by a handler that starts with a divide is legal but slow;
+and I1 had to say what latency means when the handler's first instruction
+is itself a MUL/DIV (it is *taken* within the bound, then runs normally).
 
 ### Lesson learned: free inputs must be real inputs