rabbit5 v0: own timing-predictable RV32I 5-stage core, formally verified

.github/workflows/ci.yml

@@ -18,10 +18,14 @@ jobs:
   lint:
     runs-on: ubuntu-24.04
     container: { image: "verilator/verilator:v5.054", options: --entrypoint "" }
+    strategy:
+      fail-fast: false
+      matrix:
+        core: [cv32e40p, rabbit5]
     steps:
       - uses: actions/checkout@v4
         with: { submodules: recursive }
-      - run: verilator --version && make lint
+      - run: verilator --version && make lint CORE=${{ matrix.core }}
 
   soc-sim:
     # One job per (core, program). Add cores here as rtl/cores/<name>/ adapters land.
@@ -30,7 +34,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        core: [cv32e40p]
+        core: [cv32e40p, rabbit5]
         prog: [hello]
     steps:
       - name: RISC-V GCC
@@ -45,7 +49,7 @@ jobs:
           name: soc-${{ matrix.core }}-${{ matrix.prog }}
           path: |
             dv/cocotb/soc/results.xml
-            sw/baremetal/build/${{ matrix.prog }}/${{ matrix.prog }}.dis
+            sw/baremetal/build/${{ matrix.core }}/${{ matrix.prog }}/${{ matrix.prog }}.dis
 
   ip-test:
     runs-on: ubuntu-24.04
@@ -64,6 +68,52 @@ jobs:
       - working-directory: hw_ip/sim
         run: uv run make TARGET=${{ matrix.target }}   # non-zero exit on any failed test
 
+  # riscv-formal (45 checks) + rabbit5 timing properties. ~1 min on 4 cores.
+  formal:
+    runs-on: ubuntu-24.04
+    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
+      - uses: actions/upload-artifact@v4
+        if: failure()
+        with:
+          name: formal-results
+          path: |
+            dv/formal/rabbit5/build/riscv-formal/cores/rabbit5/checks/*/logfile.txt
+            dv/formal/rabbit5/build/riscv-formal/cores/rabbit5/checks/*/engine_0/*.vcd
+            dv/formal/rabbit5/timing/timing_*/logfile.txt
+            dv/formal/rabbit5/timing/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
+    steps:
+      - uses: actions/checkout@v4
+      - uses: YosysHQ/setup-oss-cad-suite@v3
+        with: { version: "2026-11-04" }
+      - run: make gls-netlist CORE=rabbit5
+      - uses: actions/upload-artifact@v4
+        with: { name: gls-netlist-rabbit5, path: build/gls/rabbit5 }
+
+  gls-smoke:
+    needs: gls-netlist
+    runs-on: ubuntu-24.04
+    container: { image: "verilator/verilator:v5.054", options: --entrypoint "" }
+    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-rabbit5, path: build/gls/rabbit5 }
+      - run: uv sync
+      - working-directory: dv/cocotb/soc
+        run: uv run make CORE=rabbit5 PROG=hello GLS=1
+
   rma-smoke:
     runs-on: ubuntu-24.04
     steps:

.gitignore

@@ -35,3 +35,7 @@ assets/**
 sw/baremetal/build/
 **/sim_build_*/
 **/*.fst
+build/
+dv/formal/rabbit5/build/
+dv/formal/rabbit5/timing/timing_*/
+dv/formal/rabbit5/timing/timing/

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "third_party/cv32e40p"]
 	path = third_party/cv32e40p
 	url = https://github.com/openhwgroup/cv32e40p.git
+[submodule "third_party/riscv-formal"]
+	path = third_party/riscv-formal
+	url = https://github.com/YosysHQ/riscv-formal.git

Makefile

@@ -5,6 +5,8 @@
 #   make ip-test        run every hw_ip cocotb unit/integration test
 #   make lint           Verilator lint of the SoC
 #   make rma-smoke      run all rma_analysis example configs
+#   make formal         riscv-formal + timing properties (CORE=rabbit5 only)
+#   make gls-smoke      synthesize the core with Yosys, run firmware on the netlist
 #   make ci             everything CI runs
 REPO := $(abspath .)
 export REPO
@@ -20,7 +22,7 @@ IP_TARGETS := pwm_unit qei_unit telemetry_rx telemetry_tx wb_telemetry rf_cdc \
 RMA_XFAIL := fifo_same_priority_interference.yaml
 
 help:
-	@sed -n '2,9p' Makefile | sed 's/^# //'
+	@sed -n '2,11p' Makefile | sed 's/^# //'
 
 sync:
 	uv sync
@@ -58,11 +60,34 @@ rma-smoke: sync
 	  uv run rma_analysis $$f >/dev/null && echo "ok    $$f"; \
 	done
 
+# ---- formal (rabbit5) ---------------------------------------------------------
+formal:
+	$(MAKE) -C dv/formal/rabbit5
+
+# ---- gate-level smoke test: generic Yosys gates, zero delay ----------------------
+# Catches RTL that simulates differently from what synthesizes (latches, X,
+# initial values, simulation-only constructs) long before a real PDK flow.
+GLS_DIR := build/gls/$(CORE)
+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)
+	@mkdir -p $(GLS_DIR)
+	yosys $(YOSYS_SLANG) -q -l $(GLS_DIR)/synth.log -p "read_slang \
+	    $$(grep -v '^//' rtl/cores/$(CORE)/files.f | sed 's|$${REPO}|$(REPO)|' | tr '\n' ' ') \
+	    --top rabbit_cpu -DSYNTHESIS; \
+	  synth -top rabbit_cpu -flatten; tee -o $(GLS_DIR)/stat.txt stat; \
+	  write_verilog -noattr $@"
+	@grep -E '^ +[0-9]+ +cells' $(GLS_DIR)/stat.txt | head -1
+
+gls-smoke: sync gls-netlist
+	cd dv/cocotb/soc && uv run $(MAKE) CORE=$(CORE) PROG=$(PROG) GLS=1
+
 ci: lint soc-sim ip-test rma-smoke
 
 clean:
 	$(MAKE) -C sw/baremetal clean
 	cd dv/cocotb/soc && rm -rf sim_build_* results.xml dump.fst
+	rm -rf build dv/formal/rabbit5/build dv/formal/rabbit5/timing/timing_*
 	cd hw_ip/sim && uv run $(MAKE) clean
 
-.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke ci clean
+.PHONY: help sync firmware soc-sim soc-waves ip-test lint rma-smoke formal gls-netlist gls-smoke ci clean

README.md

@@ -2,20 +2,25 @@
 
 An open, verifiable **real-time RISC-V SoC** for robotics: RTL → verification →
 FPGA → open-source ASIC, evaluated with Zephyr and real-time Linux, with a
-vector / quantized-NN block. Five-year plan:
-[`docs/research/2026-11-04-soc-5yr-plan.md`](docs/research/2026-11-04-soc-5yr-plan.md).
+vector / quantized-NN block. Five-year plan and research notes are kept
+outside the repository.
 
-Baseline CPU: **OpenHW CV32E40P** (RV32IMC). Every layer above the CPU talks to
-a core-agnostic `rabbit_cpu` contract, so other cores (Ibex, CV32E40X, our own
-5-stage core) plug in the same way: [`rtl/cores/README.md`](rtl/cores/README.md).
+CPUs: **rabbit5**, our own timing-predictable 5-stage RV32I core
+([`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:
+[`rtl/cores/README.md`](rtl/cores/README.md).
 
 ## Quick start
 
 ```bash
 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 ci          # everything CI runs
+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 gls-smoke CORE=rabbit5  # same firmware on the synthesized gate netlist
+make ci                      # lint + simulation tests
 ```
 
 Walkthrough: [`docs/GETTING_STARTED.md`](docs/GETTING_STARTED.md) ·

asic/README.md

@@ -4,4 +4,4 @@
   learn LibreLane end to end.
 - Y4: full MCU SoC on an IHP or sky130 (ChipFoundry) shuttle.
 - Keep RTL PDK-portable (no vendor macros in core logic; SRAMs behind a wrapper).
-Shuttle landscape as of 2026: see `docs/research/2026-11-04-soc-5yr-plan.md` §1.6.
+Shuttle landscape as of 2026 (Efabless closed; Tiny Tapeout on IHP; sky130 via ChipFoundry): see the research notes kept outside the repo.

docs/GETTING_STARTED.md

@@ -26,7 +26,7 @@ make ci          # lint + SoC firmware sim + 10 hw_ip tests + rma_analysis examp
 | 1 | `sw/baremetal/hello/main.c` | The C program: prints, self-checks, cycle count |
 | 2 | `sw/baremetal/common/crt0.S` | Reset → stack → zero .bss → `main` → write exit code |
 | 3 | `sw/baremetal/common/link.ld` | Vectors at 0x0, code at 0x80 (CPU boot address) |
-| 4 | `sw/baremetal/build/hello/hello.dis` | The actual instructions (after `make firmware`) |
+| 4 | `sw/baremetal/build/cv32e40p/hello/hello.dis` | The actual instructions (after `make firmware`) |
 | 5 | `rtl/soc/rabbit_soc_sim.sv` | CPU + RAM + sim-control, address decode |
 | 6 | `rtl/cores/cv32e40p/rabbit_cpu.sv` | How a vendor core is plugged into our contract |
 | 7 | `dv/cocotb/soc/test_soc.py` | Testbench: clock, reset, console capture, pass/fail |

docs/STATUS.md

@@ -1,4 +1,4 @@
-# Status (updated 2026-11-04)
+# Status (updated 2026-11-06)
 
 ## Works
 
@@ -10,6 +10,19 @@
 | 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 |
 
+## rabbit5 (own core) — M0 done on branch `rabbit5-m0`
+
+| Item | Command | Result |
+|---|---|---|
+| hello on rabbit5 (RV32I, 5-stage) | `make soc-sim CORE=rabbit5` | PASS, 3958 cycles |
+| riscv-formal | `make formal` | 45/45 PASS |
+| timing properties T1–T3 + covers | `make formal` | PASS (BMC 24) |
+| gate-level smoke (Yosys generic netlist) | `make gls-smoke CORE=rabbit5` | PASS, same 3958 cycles |
+
+Next (M1/M2): enable riscv-formal CSR checks, timer + external interrupt with a
+proven entry-latency bound, RISCOF compliance, then the dual-core TDM work (M4).
+Review guide: `rtl/cores/rabbit5/README.md`.
+
 ## Known issues
 
 - `hw_ip/sim` targets `telemetry_rf` and `top` need
@@ -29,6 +42,7 @@
 - [x] Bare-metal toolchain flow (GCC → hex → $readmemh)
 - [x] Firmware-driven cocotb SoC test
 - [x] CI pipeline
+- [x] Own core rabbit5 v0 with riscv-formal, timing properties, GLS smoke (2026-11-06)
 - [ ] Machine timer (mtime/mtimecmp) + interrupt test (irq_i already exposed)
 - [ ] OBI→Wishbone bridge; attach PWM / QEI / telemetry to the CPU
 - [ ] UART (needed for FPGA and Zephyr console)

dv/cocotb/soc/Makefile

@@ -8,7 +8,7 @@ PROG ?= hello
 
 include $(REPO)/rtl/cores/$(CORE)/core.mk
 
-FIRMWARE := $(REPO)/sw/baremetal/build/$(PROG)/$(PROG).hex
+FIRMWARE := $(REPO)/sw/baremetal/build/$(CORE)/$(PROG)/$(PROG).hex
 export RABBIT_FIRMWARE := $(FIRMWARE)
 export RABBIT_PROG := $(PROG)
 
@@ -19,9 +19,16 @@ COCOTB_TEST_MODULES = test_soc
 SIM_BUILD      ?= sim_build_$(CORE)
 
 # Sources come from the per-core and SoC file lists (${REPO} is expanded by Verilator).
+# GLS=1 replaces the core RTL by its gate-level netlist (see `make gls-netlist`).
 VERILOG_SOURCES =
-EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f -f $(REPO)/rtl/soc/files.f
-EXTRA_ARGS += $(CORE_VERILATOR_FLAGS) -DRABBIT_QUIET
+ifeq ($(GLS),1)
+NETLIST    := $(REPO)/build/gls/$(CORE)/rabbit_cpu_netlist.v
+EXTRA_ARGS += $(NETLIST) -Wno-fatal -DRABBIT_GLS
+SIM_BUILD   = sim_build_$(CORE)_gls
+else
+EXTRA_ARGS += -f $(REPO)/rtl/cores/$(CORE)/files.f $(CORE_VERILATOR_FLAGS)
+endif
+EXTRA_ARGS += -f $(REPO)/rtl/soc/files.f -DRABBIT_QUIET
 ifeq ($(WAVES),1)
 # Build with tracing, switch it on at run time, and keep a separate build dir
 # (a traced model is slower, so the normal build stays trace-free).

dv/formal/README.md

@@ -1,8 +1,39 @@
-# dv/formal — formal verification (planned)
-
-- SymbiYosys properties for our own RTL first: OBI protocol (req held until
-  gnt, exactly one rvalid per granted request), address decode, sim-control.
-- Coprocessor-port handshake properties when the VPU lands (Y2).
-- **riscv-formal** for rabbit5 (Y1 H2), via its RVFI port.
-- Long term: bounded proofs of worst-case interrupt latency (see
-  `docs/research/2026-11-04-soc-5yr-plan.md` §6).
+# dv/formal — formal verification
+
+## rabbit5 (working)
+
+```bash
+make formal                       # from the repo root: everything below (~35 s on 22 cores)
+make -C dv/formal/rabbit5 riscv-formal
+make -C dv/formal/rabbit5 timing
+make -C dv/formal/rabbit5 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), `pc_fwd`/`pc_bwd` (branches, flushes), `causal`, `unique`, `liveness`, `ill` | `rabbit5/checks.cfg`, `rabbit5/wrapper.sv` |
+| **timing properties** (ours) | T1 exact retirement-gap model, T2 first retirement at cycle 5, T3 memory used exactly one cycle before retirement; covers prove every case and the 6..16 throughput bounds are reachable | `rabbit5/timing/` |
+
+How it fits together:
+1. rabbit5 is written in modern SystemVerilog. riscv-formal reads cores with
+   Yosys' built-in parser, so the Makefile first converts the core with the
+   **slang** frontend into one plain Verilog file (`build/rabbit5_flat.v`).
+2. `genchecks.py` expects `<riscv-formal>/cores/<core>/`; the Makefile builds a
+   small mirror in `build/` (symlinks to the submodule), so the submodule is
+   never modified.
+3. The timing proof reads the SystemVerilog directly through slang (≈10 s;
+   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.
+
+Mutation results (to show the checks are not vacuous):
+- forwarding priority MEM/WB swapped → only `reg_ch0` fails;
+- stall on every EX dependency (not just loads) → timing T1 fails, riscv-formal passes.
+
+## Planned
+
+- CSR checks (`csrw`, `csrc_*`) when interrupts land (M2).
+- SymbiYosys properties for the OBI bus and the SoC address decode.
+- Dual core (M4): TDM arbiter bound (n+1 cycles) and per-core timing independence.

dv/formal/rabbit5/Makefile

@@ -0,0 +1,64 @@
+# Run riscv-formal on rabbit5.
+#   make            riscv-formal checks + rabbit5 timing properties
+#   make riscv-formal   only the riscv-formal checks (parallel)
+#   make timing         only the timing properties
+#   make generate   only (re)generate the .sby files
+#   make check C=insn_add_ch0   run one check by name
+REPO   ?= $(abspath ../../..)
+RF_SRC := $(REPO)/third_party/riscv-formal
+RTL    := $(REPO)/rtl/cores/rabbit5
+BUILD  := build
+# genchecks.py expects <riscv-formal>/cores/<core>/, so build a small mirror
+MIRROR := $(BUILD)/riscv-formal
+CORE_DIR := $(MIRROR)/cores/rabbit5
+JOBS   ?= $(shell nproc)
+FLAT   := $(BUILD)/rabbit5_flat.v
+# slang is built into some Yosys builds and a plugin in others (OSS CAD Suite)
+YOSYS_SLANG := $(shell yosys -p 'help read_slang' >/dev/null 2>&1 || echo -m slang)
+
+SOURCES := $(addprefix $(RTL)/,rabbit5_pkg.sv rabbit5_decoder.sv rabbit5_alu.sv \
+             rabbit5_regfile.sv rabbit5_csr.sv rabbit5_core.sv)
+
+all: riscv-formal timing
+
+riscv-formal: generate
+	$(MAKE) -C $(CORE_DIR)/checks -j$(JOBS) -k
+	@python3 summary.py $(CORE_DIR)/checks
+
+# rabbit5's own timing properties (timing/rabbit5_timing_tb.sv)
+timing: $(BUILD)/slang_load.ys
+	cd timing && sby -f timing.sby
+
+$(BUILD)/slang_load.ys:
+	@mkdir -p $(BUILD)
+	@if [ -n "$(YOSYS_SLANG)" ]; then echo "plugin -i slang" > $@; else echo "# slang is built in" > $@; fi
+
+generate: $(CORE_DIR)/checks/makefile
+
+# 1. rabbit5 is modern SystemVerilog; riscv-formal reads files with Yosys'
+#    built-in parser, so convert once with the slang frontend.
+$(FLAT): $(SOURCES)
+	@mkdir -p $(BUILD)
+	yosys $(YOSYS_SLANG) -q -p "read_slang $(SOURCES) --top rabbit5_core -DSYNTHESIS; \
+	             hierarchy -top rabbit5_core; proc; flatten; opt_clean; \
+	             write_verilog -noattr $@"
+
+# 2. mirror + config, 3. generate one .sby per check
+$(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv
+	@mkdir -p $(MIRROR) $(CORE_DIR)
+	cp $(FLAT) $(CORE_DIR)/
+	ln -sfn $(RF_SRC)/checks $(MIRROR)/checks
+	ln -sfn $(RF_SRC)/insns  $(MIRROR)/insns
+	cp checks.cfg wrapper.sv $(CORE_DIR)/
+	rm -rf $(CORE_DIR)/checks
+	cd $(CORE_DIR) && python3 ../../checks/genchecks.py
+
+# run a single check, e.g.  make check C=insn_add_ch0
+check: generate
+	$(MAKE) -C $(CORE_DIR)/checks $(C)
+	@cat $(CORE_DIR)/checks/$(C)/status
+
+clean:
+	rm -rf $(BUILD) timing/timing_bmc timing/timing_cover timing/timing
+
+.PHONY: all riscv-formal timing generate check clean