diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 10068fc..0a5f60f 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index d97f3a3..6c581d6 100644 --- a/.gitignore +++ b/.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_*/ diff --git a/Makefile b/Makefile index f995e01..dd2a1cc 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index 4394185..0bf7e44 100644 --- a/README.md +++ b/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 `) | | `rt_rabbit/zephyr-fw/` | Zephyr control firmware | | `third_party/` | Git submodules (CV32E40P) | diff --git a/docs/STATUS.md b/docs/STATUS.md index 3409ef3..d0110c3 100644 --- a/docs/STATUS.md +++ b/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/`) diff --git a/dv/cocotb/soc/test_soc.py b/dv/cocotb/soc/test_soc.py index 63b8d75..a11086d 100644 --- a/dv/cocotb/soc/test_soc.py +++ b/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): diff --git a/dv/formal/README.md b/dv/formal/README.md index 09ee109..4ee06fb 100644 --- a/dv/formal/README.md +++ b/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.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 diff --git a/dv/formal/rabbit/Makefile b/dv/formal/rabbit/Makefile index 13893ae..4047214 100644 --- a/dv/formal/rabbit/Makefile +++ b/dv/formal/rabbit/Makefile @@ -1,7 +1,9 @@ # Formal verification of a rabbit core: make CORE=rabbit3 (default rabbit5) -# make riscv-formal checks + timing properties +# make riscv-formal checks + timing properties + muldiv # make riscv-formal only riscv-formal (parallel) # make timing only the timing properties (timing/rabbit_timing_tb.sv) +# make muldiv only the multiply/divide unit proof (muldiv/, any core) +# make muldiv-sim ... its exhaustive 8-bit simulation part # make check C=insn_add_ch0 one riscv-formal check REPO ?= $(abspath ../../..) CORE ?= rabbit5 @@ -22,7 +24,7 @@ CORE_DIR := $(MIRROR)/cores/$(CORE) # 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) -all: riscv-formal timing +all: riscv-formal timing muldiv # ---- riscv-formal -------------------------------------------------------------- riscv-formal: generate @@ -33,9 +35,12 @@ generate: $(CORE_DIR)/checks/makefile # The cores are modern SystemVerilog; riscv-formal reads files with Yosys' # built-in parser, so convert once with the slang frontend. -$(FLAT): $(SOURCES) +# M extension: riscv-formal checks MUL/DIV with stand-in results (ALTOPS) and +# a short divider (FORMAL_DIV_STEPS); the real arithmetic is the muldiv proof. +FORMAL_DEFINES := -DSYNTHESIS -DRISCV_FORMAL_ALTOPS -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS) +$(FLAT): $(SOURCES) $(REPO)/rtl/cores/$(CORE)/core.mk @mkdir -p $(BUILD) - yosys $(YOSYS_SLANG) -q -p "read_slang $(SOURCES) --top $(CORE)_core -DSYNTHESIS; \ + yosys $(YOSYS_SLANG) -q -p "read_slang $(SOURCES) --top $(CORE)_core $(FORMAL_DEFINES); \ hierarchy -top $(CORE)_core; proc; flatten; opt_clean; \ write_verilog -noattr $@" @@ -45,6 +50,7 @@ $(CORE_DIR)/checks/makefile: $(FLAT) checks.cfg wrapper.sv $(REPO)/rtl/cores/$(C ln -sfn $(RF_SRC)/insns $(MIRROR)/insns cp $(FLAT) wrapper.sv $(CORE_DIR)/ sed -e 's/@RABBIT_CORE@/$(CORE)_core/' \ + -e 's/@LIVENESS_DEPTH@/$(FORMAL_LIVENESS_DEPTH)/' \ -e 's/@RABBIT_IRQ_DEFINE@/$(if $(filter-out 0,$(TIMING_IRQ_LATENCY)),`define RABBIT_HAS_IRQ)/' \ checks.cfg > $(CORE_DIR)/checks.cfg rm -rf $(CORE_DIR)/checks @@ -57,12 +63,14 @@ check: generate # ---- timing properties ------------------------------------------------------------ # Reads the SystemVerilog through slang directly (much faster to solve than # the converted file). The core's timing model comes from its core.mk. -TIMING_DEFINES := -DSYNTHESIS -DRABBIT_CORE=$(CORE)_core \ +TIMING_DEFINES := -DSYNTHESIS -DRISCV_FORMAL_ALTOPS -DRABBIT_CORE=$(CORE)_core \ -DFIRST_RETIRE=$(TIMING_FIRST_RETIRE) \ -DREDIRECT_GAP=$(TIMING_REDIRECT_GAP) \ -DLOADUSE_GAP=$(TIMING_LOADUSE_GAP) \ -DIRQ_LATENCY=$(TIMING_IRQ_LATENCY) \ - -DCOMMIT_TO_RETIRE=$(TIMING_COMMIT_TO_RETIRE) + -DCOMMIT_TO_RETIRE=$(TIMING_COMMIT_TO_RETIRE) \ + -DMUL_CYCLES=$(TIMING_MUL_CYCLES) \ + -DRABBIT_DIV_STEPS=$(FORMAL_DIV_STEPS) timing: $(BUILD)/timing.sby cd $(BUILD) && sby -f timing.sby @@ -75,7 +83,26 @@ $(BUILD)/timing.sby: timing/timing.sby.in timing/rabbit_timing_tb.sv $(SOURCES) -e 's|@DEFINES@|$(TIMING_DEFINES)|' timing/timing.sby.in > $@ printf '%s\n' $(SOURCES) $(abspath timing/rabbit_timing_tb.sv) $(abspath $(BUILD))/slang_load.ys >> $@ +# ---- multiply/divide unit (shared by every rabbit core) ------------------------------- +# muldiv: formal (muldiv/muldiv.sby): values for every input at W = 4 / 6, +# exact latency at W = 32 +# muldiv-sim: every input at W = 8 in Verilator (muldiv/exhaustive_tb.sv). +# Warnings are shown but not fatal here: a newer Verilator adding a +# warning to this testbench must not break a proof run (the RTL itself +# is linted strictly by `make lint`). +MULDIV_RTL := $(REPO)/rtl/cores/rabbit_common/rabbit_muldiv.sv +muldiv: muldiv-sim + cd muldiv && sby -f muldiv.sby + +muldiv-sim: + @mkdir -p build/muldiv + verilator --binary --timing -Wall -Wno-fatal -Wno-DECLFILENAME -Wno-UNUSEDSIGNAL -Wno-PROCASSINIT \ + --top-module exhaustive_tb -Mdir build/muldiv -o exhaustive \ + $(MULDIV_RTL) muldiv/exhaustive_tb.sv > build/muldiv/build.log + build/muldiv/exhaustive | tee build/muldiv/run.log | grep -E 'FAIL|exhaustive|RESULT' + @grep -q 'RESULT: PASS' build/muldiv/run.log + clean: - rm -rf build + rm -rf build muldiv/muldiv_*/ muldiv/muldiv/ -.PHONY: all riscv-formal generate check timing clean +.PHONY: all riscv-formal generate check timing muldiv muldiv-sim clean diff --git a/dv/formal/rabbit/checks.cfg b/dv/formal/rabbit/checks.cfg index b943801..32676f0 100644 --- a/dv/formal/rabbit/checks.cfg +++ b/dv/formal/rabbit/checks.cfg @@ -3,9 +3,15 @@ # # [depth] columns: [start] [step to check at] (BMC cycles) # The first instruction retires 3 (rabbit3) or 5 (rabbit5) cycles after reset. +# MUL/DIV: checked with ALTOPS stand-in results and a 4-cycle divide +# (FORMAL_DIV_STEPS in core.mk); both fit in these depths. +# liveness needs a longer window since M: a divide can be interrupted in its +# last cycle and the handler may start with a divide too (it cannot be +# interrupted again: MIE = 0 in the handler), so the next retirement can be +# ~3 + 7 + 3 cycles away on rabbit5. Per core: FORMAL_LIVENESS_DEPTH (core.mk). [options] -isa rv32i +isa rv32im [depth] insn 12 @@ -14,7 +20,7 @@ pc_fwd 10 15 pc_bwd 10 15 unique 1 10 15 causal 10 15 -liveness 1 8 15 +liveness 1 8 @LIVENESS_DEPTH@ ill 12 cover 1 10 @@ -23,6 +29,7 @@ reg_ch0 [defines] `define RISCV_FORMAL_ALIGNED_MEM +`define RISCV_FORMAL_ALTOPS `define RABBIT_CORE @RABBIT_CORE@ @RABBIT_IRQ_DEFINE@ @@ -37,6 +44,7 @@ reg_ch0 # (asking riscv-formal's bigger testbench for exact counts took up to 14 min). always @* if (!reset) cover (channel[0].cnt_insns >= 4); always @* if (!reset) cover (channel[0].valid && channel[0].trap); +always @* if (!reset) cover (channel[0].valid && channel[0].insn[6:0] == 7'b0110011 && channel[0].insn[31:25] == 7'b0000001 && channel[0].insn[14]); `ifdef RABBIT_HAS_IRQ always @* if (!reset) cover (channel[0].valid && channel[0].intr); `endif diff --git a/dv/formal/rabbit/muldiv/exhaustive_tb.sv b/dv/formal/rabbit/muldiv/exhaustive_tb.sv new file mode 100644 index 0000000..a645784 --- /dev/null +++ b/dv/formal/rabbit/muldiv/exhaustive_tb.sv @@ -0,0 +1,95 @@ +// ============================================================================= +// rabbit_muldiv — exhaustive simulation at W = 8 (proof by trying everything) +// ============================================================================= +// Every op x every rs1 x every rs2 = 8 x 256 x 256 = 524 288 instructions, each +// checked against the RISC-V definition, and each must take exactly 2 (MUL*) +// or W+2 (DIV*) cycles. Every 7th instruction is first interrupted after a +// pseudo-random number of cycles (req drops for one cycle) and then restarted, +// as the pipeline does after MRET. +// +// SAT solvers are bad at multipliers (muldiv_tb.sv proves W = 6 formally); +// at 8 bits trying all inputs takes a second. Run: make -C dv/formal/rabbit muldiv-sim +// ============================================================================= +module exhaustive_tb; + localparam int W = 8; + + logic clk = 1'b0, rst_n = 1'b0; + logic req = 1'b0, done; + logic [2:0] op = '0; + logic [W-1:0] a = '0, b = '0, result; + + rabbit_muldiv #(.W(W)) dut ( + .clk_i(clk), .rst_ni(rst_n), + .en_i(req), .req_i(req), .op_i(op), .a_i(a), .b_i(b), + .done_o(done), .result_o(result) + ); + + always #5 clk = ~clk; + + function automatic logic [W-1:0] expected(input logic [2:0] o, input logic [W-1:0] x, y); + logic signed [W:0] ex, ey; + logic signed [2*W+1:0] p; + logic ovf; + ex = {o[1:0] != 2'b11 && x[W-1], x}; + ey = {o[1:0] <= 2'b01 && y[W-1], y}; + p = ex * ey; + ovf = (x == {1'b1, {(W-1){1'b0}}}) && (y == '1); + unique case (o) + 3'd0: return p[W-1:0]; + 3'd1, 3'd2, + 3'd3: return p[2*W-1:W]; + 3'd4: return (y == 0) ? '1 : ovf ? x : W'($signed(x) / $signed(y)); + 3'd5: return (y == 0) ? '1 : x / y; + 3'd6: return (y == 0) ? x : ovf ? '0 : W'($signed(x) % $signed(y)); + default: return (y == 0) ? x : x % y; + endcase + endfunction + + int errors = 0, runs = 0, kills = 0; + int unsigned lfsr = 32'h1; + + initial begin + @(posedge clk); #1 rst_n = 1'b1; + for (int o = 0; o < 8; o++) begin + for (int x = 0; x < 2**W; x++) begin + for (int y = 0; y < 2**W; y++) begin + automatic int cycles, want; + automatic logic [W-1:0] got; + op = 3'(o); a = W'(x); b = W'(y); + want = op[2] ? W + 2 : 2; + runs++; + lfsr = lfsr ^ (lfsr << 13); lfsr = lfsr ^ (lfsr >> 17); lfsr = lfsr ^ (lfsr << 5); + if (runs % 7 == 0) begin // interrupt it, then start again + automatic int stop_after = int'(lfsr % unsigned'(want - 1)) + 1; + req = 1'b1; + repeat (stop_after) @(posedge clk); + #1 req = 1'b0; + @(posedge clk); #1; + kills++; + end + // run to completion, checking the cycle where done_o is high + req = 1'b1; + cycles = 0; + forever begin + #3; // settle (combinational outputs) + cycles++; + if (done) begin got = result; break; end + @(posedge clk); #1; + if (cycles > want) break; + end + @(posedge clk); #1 req = 1'b0; + if (cycles != want || got !== expected(op, a, b)) begin + if (errors < 10) + $display("FAIL op=%0d a=%02x b=%02x got=%02x expected=%02x cycles=%0d (want %0d)", + op, a, b, got, expected(op, a, b), cycles, want); + errors++; + end + end + end + end + $display("muldiv exhaustive W=%0d: %0d instructions (%0d interrupted first), %0d errors", + W, runs, kills, errors); + $display("RESULT: %s", errors == 0 ? "PASS" : "FAIL"); + $finish; + end +endmodule diff --git a/dv/formal/rabbit/muldiv/muldiv.sby b/dv/formal/rabbit/muldiv/muldiv.sby new file mode 100644 index 0000000..04d6f2d --- /dev/null +++ b/dv/formal/rabbit/muldiv/muldiv.sby @@ -0,0 +1,40 @@ +# Unit proof of rtl/cores/rabbit_common/rabbit_muldiv.sv (see muldiv_tb.sv) +# make -C dv/formal/rabbit muldiv (also runs the exhaustive 8-bit simulation) +# +# prove4 W = 4 values + latency, every input, ANY length of history (PDR) +# bmc6 W = 6 values + latency, every input, all histories up to 20 cycles +# lat32 W = 32 exact latency, any length of history (PDR) +# cover6 W = 6 the interesting cases really happen (x/0, overflow, ...) +# +# Bit-level ABC engines: on multipliers they are much faster than the SMT +# solvers used elsewhere (boolector needed >10 min for W = 8 at step 14). +[tasks] +prove4 +bmc6 +lat32 +cover6 + +[options] +prove4: mode prove +bmc6: mode bmc +bmc6: depth 20 +lat32: mode prove +cover6: mode cover +cover6: depth 20 + +[engines] +prove4: abc pdr +bmc6: abc bmc3 +lat32: abc pdr +cover6: smtbmc boolector + +[script] +prove4: read_slang rabbit_muldiv.sv muldiv_tb.sv --top muldiv_tb -DW=4 -DCHECK_VALUES +bmc6: read_slang rabbit_muldiv.sv muldiv_tb.sv --top muldiv_tb -DW=6 -DCHECK_VALUES +cover6: read_slang rabbit_muldiv.sv muldiv_tb.sv --top muldiv_tb -DW=6 -DCHECK_VALUES +lat32: read_slang rabbit_muldiv.sv muldiv_tb.sv --top muldiv_tb -DW=32 +prep -top muldiv_tb + +[files] +../../../../rtl/cores/rabbit_common/rabbit_muldiv.sv +muldiv_tb.sv diff --git a/dv/formal/rabbit/muldiv/muldiv_tb.sv b/dv/formal/rabbit/muldiv/muldiv_tb.sv new file mode 100644 index 0000000..1dce3f5 --- /dev/null +++ b/dv/formal/rabbit/muldiv/muldiv_tb.sv @@ -0,0 +1,109 @@ +// ============================================================================= +// rabbit_muldiv — unit proof: the arithmetic and the fixed latency +// ============================================================================= +// riscv-formal cannot check multiplication or division (it uses stand-in +// results, ALTOPS). This proof checks the real arithmetic on the very same +// RTL, at widths where the solver can try EVERY input (muldiv.sby): +// +// A1 the result equals the RISC-V definition (x/0 and overflow included) +// L1 done_o comes exactly 2 (MUL*) / W+2 (DIV*) cycles after the +// instruction arrived, never earlier, never later +// for every op, every pair of operands and ANY interrupt pattern (req_i +// may drop in any cycle; the instruction then starts again from scratch) +// +// W = 4 A1 + L1, for histories of any length (PDR, unbounded) +// W = 6 A1 + L1, all histories up to 20 cycles (BMC) +// W = 8 A1 + L1, all 524 288 instructions in simulation (exhaustive_tb.sv) +// W = 32 L1, for histories of any length (PDR); A1 only in simulation +// (sw/baremetal/muldiv: corner cases + random operands, every core) +// +// rabbit_muldiv is written for any even W, and its structure (two half +// multiplies, one quotient bit per step) is the same at every width. SAT +// solvers cannot prove 32-bit multipliers equal (they blow up beyond ~8 bits); +// see dv/formal/README.md. +// ============================================================================= +module muldiv_tb ( + input logic clk, + // free inputs, chosen by the solver every cycle (see timing tb for why + // they are ports and not (* anyseq *) signals) + input logic en, // an M instruction is in execute ... + input logic req, // ... and is not being interrupted + input logic [2:0] op, + input logic [`W-1:0] a, + input logic [`W-1:0] b +); + localparam int W = `W; + + logic rst_n = 1'b0; + always_ff @(posedge clk) rst_n <= 1'b1; + + logic done; + logic [W-1:0] result; + rabbit_muldiv #(.W(W)) dut ( + .clk_i(clk), .rst_ni(rst_n), + .en_i(en), .req_i(req), .op_i(op), .a_i(a), .b_i(b), + .done_o(done), .result_o(result) + ); + + // ---- the contract with the pipeline: an instruction that is still being + // worked on keeps its op and operands (it may be dropped: req = 0) ---- + logic held; + logic [2:0] op_q; + logic [W-1:0] a_q, b_q; + always_ff @(posedge clk) begin + held <= rst_n && req && !done; + op_q <= op; a_q <= a; b_q <= b; + end + always_comb if (rst_n && held && req) assume (op == op_q && a == a_q && b == b_q); + always_comb assume (en || !req); // the pipeline never asks without an M instruction + + // ---- L1: exact latency ---------------------------------------------------- + int n; // cycles the current instruction has already spent in the unit + always_ff @(posedge clk) begin + if (!rst_n || !req || done) n <= 0; + else n <= n + 1; + end + always_comb if (rst_n && req) assert (done == (n == (op[2] ? W + 1 : 1))); // L1 + always_comb if (rst_n && !req) assert (!done); + +`ifdef CHECK_VALUES + // ---- A1: the RISC-V definition ------------------------------------------------ + // one (W+1) x (W+1) signed product; the op decides how a and b are extended + logic signed [W:0] ea, eb; + logic signed [2*W+1:0] p; + assign ea = {op[1:0] != 2'b11 && a[W-1], a}; // rs1 signed: MUL, MULH, MULHSU + assign eb = {op[1:0] <= 2'b01 && b[W-1], b}; // rs2 signed: MUL, MULH + assign p = ea * eb; + + localparam logic [W-1:0] ONES = '1; + localparam logic [W-1:0] MIN = {1'b1, {(W-1){1'b0}}}; + logic overflow; + assign overflow = (a == MIN) && (b == ONES); + + logic [W-1:0] expected; + always_comb begin + unique case (op) + 3'd0: expected = p[W-1:0]; // MUL + 3'd1, 3'd2, + 3'd3: expected = p[2*W-1:W]; // MULH, MULHSU, MULHU + 3'd4: expected = (b == 0) ? ONES : overflow ? MIN : // DIV + W'($signed(a) / $signed(b)); + 3'd5: expected = (b == 0) ? ONES : a / b; // DIVU + 3'd6: expected = (b == 0) ? a : overflow ? '0 : // REM + W'($signed(a) % $signed(b)); + default: expected = (b == 0) ? a : a % b; // REMU + endcase + end + always_comb if (rst_n && done) assert (result == expected); // A1 +`endif + + // ---- non-vacuity ---------------------------------------------------------------- + always_comb begin + if (rst_n && done) begin + cover (op == 3'd4 && b == 0); // x / 0 + cover (op == 3'd6 && a == {1'b1, {(W-1){1'b0}}} && b == '1); // overflow + cover (op == 3'd1 && a[W-1] && b[W-1]); // negative x negative + end + if (rst_n && held && !req) cover (op_q[2]); // a divide is interrupted ... + end +endmodule diff --git a/dv/formal/rabbit/timing/rabbit_timing_tb.sv b/dv/formal/rabbit/timing/rabbit_timing_tb.sv index 4a8d844..4feba28 100644 --- a/dv/formal/rabbit/timing/rabbit_timing_tb.sv +++ b/dv/formal/rabbit/timing/rabbit_timing_tb.sv @@ -14,6 +14,10 @@ // LOADUSE_GAP cycles between a load and an instruction using it (2 / 1) // IRQ_LATENCY worst-case interrupt latency, 0 = no interrupts (7 / 4) // COMMIT_TO_RETIRE cycles from the commit stage to retirement (2 / 1) +// MUL_CYCLES cycles a MUL* spends in the commit stage (2 / 2) +// RABBIT_DIV_STEPS divider steps in this proof; a DIV* spends +// RABBIT_DIV_STEPS+2 cycles in the commit stage (see core.mk: +// the proof uses 2 steps, the real 32 are proven in muldiv/) // // T1 exact timing model: the gap between two consecutive retirements is // REDIRECT_GAP if the earlier instruction changed control flow @@ -21,7 +25,10 @@ // LOADUSE_GAP if the later one reads the register the // earlier one loaded (load-use) [rule R2] // 1 otherwise [rule R1] +// plus MUL_CYCLES-1 / DIV_CYCLES-1 if the later one is an M +// instruction, whatever its operands [rule R8] // T2 the first instruction retires exactly FIRST_RETIRE cycles after reset +// (plus the M extra cycles if it is an M instruction) // T3 a data-memory request happens exactly one cycle before the instruction // that made it retires, and never at any other time [rule R4] // T4 after WFI sleep, the next instruction retires FIRST_RETIRE-1 cycles @@ -30,7 +37,10 @@ // // Interrupts (only if the core declares IRQ_LATENCY > 0): // I1 bounded latency: an enabled interrupt that stays pending makes the -// first handler instruction retire within IRQ_LATENCY cycles +// first handler instruction retire within IRQ_LATENCY cycles (plus +// that instruction's own M extra cycles if it is a MUL/DIV: the +// interrupt is *taken* within the bound, whatever the core was doing, +// including in the middle of a divide) // I2 no spurious interrupts: an interrupt is only taken if one was pending // and enabled // I3 precise: mepc, as read by the handler, is the pc of the instruction @@ -40,6 +50,15 @@ // vector the core jumped to) // I5 the handler starts at the right address: mtvec base (direct mode) or // base + 4*line for a requested line (vectored mode) +// M extension: +// M0 while an M instruction waits in the commit stage, its operand values +// do not change (rabbit_muldiv relies on it; white-box: looks inside +// rabbit_execute) +// M1 an interrupt that arrives while an M instruction waits is taken +// within the same IRQ_LATENCY bound (I1 covers it; cover below shows +// it happens) +// M2 while an M instruction waits, no instruction is fetched (power: a +// divide costs no instruction-memory reads) // Sleep (WFI), for power: // W0 the core only falls asleep when a WFI retires // W1 it wakes in the cycle after an enabled interrupt becomes pending @@ -66,6 +85,8 @@ module rabbit_timing_tb ( localparam int REDIRECT_GAP = `REDIRECT_GAP; localparam int LOADUSE_GAP = `LOADUSE_GAP; localparam int IRQ_LATENCY = `IRQ_LATENCY; + localparam int MUL_CYCLES = `MUL_CYCLES; + localparam int DIV_CYCLES = `RABBIT_DIV_STEPS + 2; `ifndef COMMIT_TO_RETIRE `define COMMIT_TO_RETIRE 1 `endif @@ -148,6 +169,12 @@ module rabbit_timing_tb ( || (opcode == 7'b1100011 && branch_taken); // taken branch assign is_load = (opcode == 7'b0000011) && !rvfi_trap; + // M extension: extra cycles in the commit stage (rule R8) + logic is_m; + int m_extra; + assign is_m = (opcode == 7'b0110011) && (rvfi_insn[31:25] == 7'b0000001) && !rvfi_trap; + assign m_extra = !is_m ? 0 : funct3[2] ? DIV_CYCLES - 1 : MUL_CYCLES - 1; + // CSR instructions (the ISA meaning: old value -> rd, then write) logic is_csr, csr_writes; logic [11:0] csr_addr; @@ -206,17 +233,17 @@ module rabbit_timing_tb ( (rvfi_rs1_addr == prev_rd || rvfi_rs2_addr == prev_rd); int expected_gap; - assign expected_gap = prev_flow ? REDIRECT_GAP : (load_use ? LOADUSE_GAP : 1); + assign expected_gap = (prev_flow ? REDIRECT_GAP : (load_use ? LOADUSE_GAP : 1)) + m_extra; // ---- T1, T2, T4 -------------------------------------------------------------------- // An interrupt removes an instruction from the pipeline; its timing is I1. always_comb begin if (rst_n && rvfi_valid && !rvfi_intr) begin - if (!seen_one) assert (cycle == FIRST_RETIRE - 1); // T2 (cycle counts from 0) - else if (slept) assert (since_sleep + 1 + D == FIRST_RETIRE - 1); // T4 + if (!seen_one) assert (cycle == FIRST_RETIRE - 1 + m_extra); // T2 (cycle counts from 0) + else if (slept) assert (since_sleep + 1 + D == FIRST_RETIRE - 1 + m_extra); // T4 else assert (gap == expected_gap); // T1 end - if (rst_n && !seen_one) assert (cycle < FIRST_RETIRE); // T2: nothing is late + if (rst_n && !seen_one) assert (cycle < FIRST_RETIRE + DIV_CYCLES - 1); // T2: nothing is late end // ---- T3: memory is used exactly one cycle before retirement --------------------------- @@ -227,6 +254,20 @@ module rabbit_timing_tb ( if (rst_n) assert (data_req_q == (rvfi_valid && (rvfi_mem_rmask != 0 || rvfi_mem_wmask != 0))); end + // ---- M0: operands stay put while an M instruction waits ------------------------------ + logic ex_busy_q = 1'b0; + logic [31:0] ex_rs1_q, ex_rs2_q; + always_ff @(posedge clk) begin + ex_busy_q <= rst_n && dut.u_execute.busy_o; + ex_rs1_q <= dut.u_execute.rs1_i; + ex_rs2_q <= dut.u_execute.rs2_i; + end + always_comb begin + if (rst_n && ex_busy_q && dut.u_execute.valid_i) + assert (dut.u_execute.rs1_i == ex_rs1_q && dut.u_execute.rs2_i == ex_rs2_q); // M0 + if (rst_n && dut.u_execute.busy_o) assert (!instr_req); // M2 + end + // ---- interrupt-enable state: a spec model computed from RVFI only ------------------- // m_* = state after every instruction that has retired before this cycle, // n_* = ... including the one retiring now. A core changes its CSRs in the @@ -304,10 +345,22 @@ module rabbit_timing_tb ( end end always_comb begin - if (rst_n) assert (wait_cycles + D <= IRQ_LATENCY); // I1 + // I1: the handler's first instruction retires within IRQ_LATENCY, plus + // its own M extra cycles if it is itself a MUL/DIV (it cannot be + // interrupted: MIE = 0 in the handler). The second line bounds the + // wait in every cycle, so an interrupt can never be ignored. + if (rst_n && rvfi_valid && rvfi_intr) assert (wait_cycles + D <= IRQ_LATENCY + m_extra); + if (rst_n) assert (wait_cycles + D <= IRQ_LATENCY + DIV_CYCLES - 1); if (rst_n && rvfi_valid && rvfi_intr) assert (requested); // I2 end + // M1 (cover): an M instruction was waiting when the interrupt was taken + logic m_busy_seen; + always_ff @(posedge clk) begin + if (!rst_n || (rvfi_valid && rvfi_intr)) m_busy_seen <= 1'b0; + else if (ex_busy_q && dut.u_execute.irq_take) m_busy_seen <= 1'b1; // was waiting, now interrupted + end + // ---- I5: where the handler starts -------------------------------------------------- // m_tvec is mtvec as the core saw it when it took the interrupt: every // instruction retiring in between is older than the interrupted one. @@ -365,9 +418,10 @@ module rabbit_timing_tb ( // ---- non-vacuity --------------------------------------------------------------------- always_comb begin if (rst_n && rvfi_valid && rvfi_intr) begin - cover (wait_cycles + D == IRQ_LATENCY); // the bound is reached (it is tight) + cover (wait_cycles + D == IRQ_LATENCY && m_extra == 0); // the bound is tight cover (wait_cycles + D == IRQ_LATENCY - 1); cover (slept); // WFI woken by the interrupt it takes + cover (m_busy_seen); // M1: interrupt while an M op waited cover (!m_tvec[0]); // direct mode is exercised too cover (m_tvec[0] && vec_line != 7); // ... and a vector other than the timer's end @@ -382,7 +436,8 @@ module rabbit_timing_tb ( // ---- throughput bounds ------------------------------------------------------------------ // From T1 + T2: after the first retirement (cycle FIRST_RETIRE-1), one more // instruction retires every 1..REDIRECT_GAP cycles. So at cycle 19 between - // MIN_AT_19 and MAX_AT_19 have retired (rabbit5: 6..16, rabbit3: 9..18). + // MIN_AT_19 and MAX_AT_19 have retired (rabbit5: 6..16, rabbit3: 9..18), + // not counting M extra cycles and sleep. // Both extremes must be reachable (covers below). localparam int MAX_AT_19 = 19 - (FIRST_RETIRE - 1) + 1; localparam int MIN_AT_19 = (19 - (FIRST_RETIRE - 1)) / REDIRECT_GAP + 1; @@ -405,6 +460,9 @@ module rabbit_timing_tb ( cover (gap == LOADUSE_GAP && load_use); cover (gap == REDIRECT_GAP); cover (gap == REDIRECT_GAP && rvfi_trap); + cover (is_m && !funct3[2] && gap == MUL_CYCLES); // R8: multiply + cover (is_m && funct3[2] && gap == DIV_CYCLES); // R8: divide + cover (is_m && load_use); // R8 after load-use end end endmodule diff --git a/rtl/cores/README.md b/rtl/cores/README.md index 2169ecd..bf635ad 100644 --- a/rtl/cores/README.md +++ b/rtl/cores/README.md @@ -56,8 +56,8 @@ adapter, in `rtl/soc/`. | `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 | | `cv32e40x/` | OpenHW CV32E40X | planned | Brings CV-X-IF for the vector/NN coprocessor | -| `rabbit3/` | Our own 3-stage RV32I core (F/X/W) — **start here** | **working** | riscv-formal 45/45, timing + interrupt properties, interrupts + WFI, GLS smoke | -| `rabbit5/` | Our own 5-stage, timing-predictable RV32I core | **working** | riscv-formal 45/45, timing + interrupt properties, interrupts + WFI, GLS smoke | +| `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` | The contract will grow (v1) with an optional **coprocessor port** (CV-X-IF diff --git a/rtl/cores/rabbit3/README.md b/rtl/cores/rabbit3/README.md index fbe56ef..79c061b 100644 --- a/rtl/cores/rabbit3/README.md +++ b/rtl/cores/rabbit3/README.md @@ -1,4 +1,4 @@ -# rabbit3 — 3-stage RV32I core (start here) +# rabbit3 — 3-stage RV32IM core (start here) The smallest rabbit pipeline: **F | X | W**. It is built from exactly the same blocks as rabbit5 (`../rabbit_common/`); only the pipeline file differs. @@ -22,15 +22,17 @@ F ──► X ────────────────────── | 6 | `../rabbit5/rabbit5_core.sv` | what had to be *added* for two more stages: hold register, load-use stall, forwarding | | 7 | interrupts: `rabbit_csr.sv` (mie, mip, enables) → `rabbit_execute.sv` (`irq_take`) → `rabbit3_core.sv` (`sleep_q`) | why can the interrupted instruction simply be dropped? (hint: X is the commit point) | | 8 | `sw/baremetal/irq/main.c` | a timer-driven control loop with WFI, as a robot would run it | +| 9 | M extension: `rabbit_muldiv.sv` → `rabbit_execute.sv` (`busy_o`) → `rabbit3_core.sv` (`x_busy`, `x_hold_q`) | why does the instruction word need a holding register while X waits, and why are the operands still right? | Then run both and look at the difference: ```bash -make soc-sim CORE=rabbit3 # hello: 3145 cycles -make soc-sim CORE=rabbit5 # hello: 3958 cycles +make soc-sim CORE=rabbit3 # hello: 2756 cycles +make soc-sim CORE=rabbit5 # hello: 3471 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 -make formal CORE=rabbit3 # riscv-formal 45/45 + timing properties +make formal CORE=rabbit3 # riscv-formal 53/53 + timing properties + muldiv proof make gls-smoke CORE=rabbit3 # same firmware on the gate netlist ``` @@ -45,8 +47,10 @@ make gls-smoke CORE=rabbit3 # same firmware on the gate netlist | Gap between two retirements | 1 or 2 (+ sleep) | 1, 2 or 3 | | Interrupts (timer, external, 16 fast lines): worst-case latency, proven and reached | **4 cycles** | 7 cycles | | WFI sleep (`core_sleep_o` for clock gating) | yes, fetch restarts in the cycle the interrupt appears | same | -| `hello` (RV32I, software mul/div) | 3145 cycles | 3958 cycles | -| Size (Yosys generic gates, incl. adapter) | 10.4 k cells | 11.5 k cells | +| 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) | +| 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 | So rabbit3 needs fewer cycles, but each cycle must be longer. Which one is @@ -76,11 +80,41 @@ irq_i ──► mip ──AND── mie ──► "wake" ──AND── mstatus - The interrupt lines go into X without a register (lowest latency). In a real chip they must come from flip-flops in the same clock domain. +## M extension (how it works in rabbit3) + +``` +X: MUL/DIV arrives ──► rabbit_muldiv starts; busy_o = 1 + while busy: X keeps the instruction (x_hold_q: the word is kept, since + no new word is fetched), F does not fetch, W gets bubbles + last cycle: done → result goes to W like any ALU result; fetch resumes +``` + +- Operands come from the register file; while X waits, nothing writes it + (W only holds bubbles after the first cycle), so they stay the same — the + muldiv unit relies on that (checked: M0 in `dv/formal/rabbit/timing`). +- An interrupt during the wait is taken at once (R6); the M instruction runs + again from the start after MRET. +- Not fetching during the wait saves 33 instruction-memory reads per divide. + +Known limitation: **a divide can be starved by frequent interrupts.** An +interrupt abandons a running multiply/divide, which restarts from zero after +MRET. What is proven: every interrupt is taken within the latency bound (any +interrupt pattern), and a divide that sees no interrupt for 34 cycles takes +exactly 34. What is *not* guaranteed: progress. If interrupts keep arriving +more often than about 34 cycles + the handler's run time, the divide never +completes. In a response-time analysis each interrupt that hits a divide costs +up to 33 extra cycles, which needs a minimum spacing between interrupts as an +assumption (a 1-10 kHz control loop at 50 MHz is far from the limit; counting +encoder edges by interrupt would not be, so use the QEI peripheral). The +alternatives are to finish the divide first (CV32E40P: progress guaranteed, +latency +33 cycles), resume it, or abort only once; the choice is open. + ## What is shared, what is not | | Shared (`rabbit_common`) | rabbit3 only | |---|---|---| | Decode, ALU, branch decision, CSRs, traps, next pc | ✔ `rabbit_execute`, `rabbit_decoder` | | +| Multiply / divide | ✔ `rabbit_muldiv` | holding X while it works | | Register file | ✔ `rabbit_regfile` | | | RVFI reporting | ✔ `rabbit_rvfi` | | | Load/store byte lanes and sign extension | ✔ functions in `rabbit_pkg` | | diff --git a/rtl/cores/rabbit3/core.mk b/rtl/cores/rabbit3/core.mk index 1b6c797..d74bde7 100644 --- a/rtl/cores/rabbit3/core.mk +++ b/rtl/cores/rabbit3/core.mk @@ -1,5 +1,5 @@ # Per-core build settings, included by the top-level and dv Makefiles. -CORE_MARCH := rv32i_zicsr +CORE_MARCH := rv32im_zicsr CORE_MABI := ilp32 # Our own RTL: no warning suppressions. CORE_VERILATOR_FLAGS := @@ -15,3 +15,14 @@ TIMING_IRQ_LATENCY := 4 # Cycles from the commit stage (X) to retirement (W). The timing testbench # uses it to line up its RVFI-based spec model with the core. TIMING_COMMIT_TO_RETIRE := 1 +# M extension (rule R8): cycles an instruction spends in X, for any +# operands. FORMAL_DIV_STEPS is the divider's step count used by the +# pipeline-level proofs (a 34-cycle divide does not fit in their depth); the +# real 32 steps are proven in dv/formal/rabbit/muldiv (L1). +TIMING_MUL_CYCLES := 2 +TIMING_DIV_CYCLES := 34 +FORMAL_DIV_STEPS := 2 +# riscv-formal liveness: the check cycle (window = depth - 8). An interrupted +# divide plus a handler that starts with a divide needs a long window; +# measured: 16 fails (a real longer gap), 18 passes. +FORMAL_LIVENESS_DEPTH := 20 diff --git a/rtl/cores/rabbit3/files.f b/rtl/cores/rabbit3/files.f index 97bcaef..96f8b15 100644 --- a/rtl/cores/rabbit3/files.f +++ b/rtl/cores/rabbit3/files.f @@ -1,10 +1,11 @@ -// rabbit3 (RV32I, 3-stage) + shared rabbit_common blocks + rabbit_cpu adapter. +// rabbit3 (RV32IM, 3-stage) + shared rabbit_common blocks + rabbit_cpu adapter. // ${REPO} is expanded by Verilator / the Makefiles. ${REPO}/rtl/cores/rabbit_common/rabbit_pkg.sv ${REPO}/rtl/cores/rabbit_common/rabbit_decoder.sv ${REPO}/rtl/cores/rabbit_common/rabbit_alu.sv ${REPO}/rtl/cores/rabbit_common/rabbit_regfile.sv ${REPO}/rtl/cores/rabbit_common/rabbit_csr.sv +${REPO}/rtl/cores/rabbit_common/rabbit_muldiv.sv ${REPO}/rtl/cores/rabbit_common/rabbit_execute.sv ${REPO}/rtl/cores/rabbit_common/rabbit_rvfi.sv ${REPO}/rtl/cores/rabbit3/rabbit3_core.sv diff --git a/rtl/cores/rabbit3/rabbit3_core.sv b/rtl/cores/rabbit3/rabbit3_core.sv index a6439a6..2386786 100644 --- a/rtl/cores/rabbit3/rabbit3_core.sv +++ b/rtl/cores/rabbit3/rabbit3_core.sv @@ -1,5 +1,5 @@ // ============================================================================= -// rabbit3_core — 3-stage in-order RV32I pipeline (single hart) +// rabbit3_core — 3-stage in-order RV32IM pipeline (single hart) // ============================================================================= // START HERE to learn the rabbit pipelines; then read rabbit5_core.sv. // @@ -32,7 +32,8 @@ // and costs exactly 1 cycle (1 bubble). // R4 Memory must answer in exactly 1 cycle (grant in the request cycle, // data the next cycle). -// R5 Nothing else ever stalls the pipeline, except WFI sleep (R7). +// R5 Nothing else ever stalls the pipeline, except WFI sleep (R7) and +// the M extension (R8). // R6 Interrupts are taken in X, on the instruction there, which does not // retire (it runs again after MRET). The handler's first instruction // retires at most TIMING_IRQ_LATENCY cycles after an enabled interrupt @@ -40,9 +41,15 @@ // R7 WFI is a redirect to pc+4 (R3). If no enabled interrupt is pending, // fetch stops (core_sleep_o = 1) until one is; it restarts in the same // cycle the interrupt appears. +// R8 MUL/MULH/MULHSU/MULHU stay 2 cycles in X, DIV/DIVU/REM/REMU 34, +// whatever the operands: they retire 1 or 33 cycles later than +// another instruction would. Fetch stops meanwhile (no wasted memory +// reads). An interrupt is still taken at once (R6): the multiply or +// divide is abandoned and runs again after MRET. // -// So the time between two consecutive retirements is 1 or 2 cycles, plus the -// cycles spent asleep, except around an interrupt (R6). +// So the time between two consecutive retirements is 1 or 2 cycles, plus 1 +// or 33 for M instructions (R8), plus the cycles spent asleep, except around +// an interrupt (R6). // ----------------------------------------------------------------------------- // // What an instruction does lives in rtl/cores/rabbit_common/ (shared with @@ -117,8 +124,9 @@ module rabbit3_core logic x_sleep; // the instruction in X is a WFI that goes to sleep logic wake; // an enabled interrupt is pending logic fetch; // a fetch happens this cycle + logic x_busy; // X holds an unfinished multiply/divide (R8) - assign fetch = fetch_enable_i && (!sleep_q || wake); + assign fetch = fetch_enable_i && (!sleep_q || wake) && !x_busy; assign instr_req_o = fetch; assign instr_addr_o = pc_q; assign core_sleep_o = sleep_q; @@ -141,24 +149,40 @@ module rabbit3_core // =========================================================================== logic x_valid_q; // the word arriving now is a real instruction logic [31:0] x_pc_q; // ... fetched from this address + // While X is held (R8) no new word arrives, so the instruction is kept in + // a small holding register (32 flip-flops; same idea as rabbit5's ID). + logic x_hold_q; + logic [31:0] x_hold_instr_q; + logic [31:0] x_instr; + + assign x_instr = x_hold_q ? x_hold_instr_q : instr_rdata_i; always_ff @(posedge clk_i or negedge rst_ni) begin if (!rst_ni) begin - x_valid_q <= 1'b0; - x_pc_q <= '0; + x_valid_q <= 1'b0; + x_pc_q <= '0; + x_hold_q <= 1'b0; + x_hold_instr_q <= '0; end else if (redirect) begin // the word in flight is wrong-path - x_valid_q <= 1'b0; + x_valid_q <= 1'b0; + x_hold_q <= 1'b0; + end else if (x_busy) begin // keep the same instruction (R8) + x_hold_q <= 1'b1; + x_hold_instr_q <= x_instr; end else begin - x_valid_q <= fetch; - x_pc_q <= pc_q; + x_valid_q <= fetch; + x_pc_q <= pc_q; + x_hold_q <= 1'b0; end end decoded_t x_dec; - rabbit_decoder u_decoder (.instr_i(instr_rdata_i), .dec_o(x_dec)); + rabbit_decoder u_decoder (.instr_i(x_instr), .dec_o(x_dec)); // Register file: read in X, written in W. The write-first bypass inside - // is this core's entire forwarding network. + // is this core's entire forwarding network. While X is held (R8), the + // older instruction in W writes its result in the first cycle (bypass) and + // W then holds bubbles, so the operand values read here stay the same. logic [31:0] x_rs1_val, x_rs2_val; rabbit_regfile u_regfile ( .clk_i, @@ -172,13 +196,14 @@ module rabbit3_core .clk_i, .rst_ni, .valid_i (x_valid_q), .pc_i (x_pc_q), - .instr_i (instr_rdata_i), + .instr_i (x_instr), .dec_i (x_dec), .rs1_i (x_rs1_val), .rs2_i (x_rs2_val), .res_o (x_res), .redirect_o (redirect), .redirect_pc_o(redirect_pc), + .busy_o (x_busy), .irq_i, .sleep_o (x_sleep), .wake_o (wake) diff --git a/rtl/cores/rabbit3/rabbit_cpu.sv b/rtl/cores/rabbit3/rabbit_cpu.sv index 655a60a..28f10da 100644 --- a/rtl/cores/rabbit3/rabbit_cpu.sv +++ b/rtl/cores/rabbit3/rabbit_cpu.sv @@ -1,4 +1,4 @@ -// rabbit_cpu adapter for rabbit3 (our own 3-stage RV32I core). +// rabbit_cpu adapter for rabbit3 (our own 3-stage RV32IM core). // See rtl/cores/README.md for the port contract. rabbit5 needs memories that // grant immediately and answer one cycle later (rabbit3_core.sv, rule R4). module rabbit_cpu #( diff --git a/rtl/cores/rabbit5/README.md b/rtl/cores/rabbit5/README.md index 62cc8dc..357533a 100644 --- a/rtl/cores/rabbit5/README.md +++ b/rtl/cores/rabbit5/README.md @@ -1,6 +1,6 @@ -# rabbit5 — our own timing-predictable RV32I core (v0) +# rabbit5 — our own timing-predictable RV32IM core (v0) -A classic 5-stage, single-issue, in-order RV32I pipeline written to be **read, +A classic 5-stage, single-issue, in-order RV32IM pipeline written to be **read, reviewed and modified**, with one research goal: *every instruction's timing is known in advance and proven*. Plugs into the SoC through the same `rabbit_cpu` contract as CV32E40P, so both run the same firmware and tests. @@ -17,14 +17,16 @@ IF ──► ID ──► EX ──► MEM ──► WB | What | Result | Command | |---|---|---| -| `hello` firmware in the SoC | PASS, 3958 cycles (rabbit3: 3145, CV32E40P: 3450 with HW mul/div) | `make soc-sim CORE=rabbit5` | -| riscv-formal (37 instructions + reg, pc_fwd, pc_bwd, causal, unique, liveness, ill, cover) | **45/45 PASS** | `make formal CORE=rabbit5` | +| `hello` firmware in the SoC | PASS, 3471 cycles (RV32I: 3958; rabbit3: 2756, CV32E40P: 3450) | `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 3958, irq 9025) | `make gls-smoke CORE=rabbit5` | +| Gate-level smoke test (Yosys generic gates) | PASS, **same cycles** as RTL (hello 3471, irq 9025, muldiv) | `make gls-smoke CORE=rabbit5` | | Verilator `-Wall` lint | clean | `make lint CORE=rabbit5` | -| Size (Yosys generic synthesis, core + adapter) | ≈ 11.5 k cells | `make gls-netlist 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` | > Correction (2026-11-06): the first version of the timing testbench declared > its free inputs with `(* anyseq *)`, which the slang frontend silently @@ -53,7 +55,8 @@ Then: 4. **R4** memory grants immediately and answers after exactly 1 cycle (scratchpad assumption); 5. **R5** nothing else stalls, except WFI sleep; 6. **R6** an interrupt is taken in EX on the instruction there (it does not retire; MRET runs it later): latency ≤ 7 cycles; -7. **R7** WFI = redirect to pc+4, then sleep until an enabled interrupt is pending (`core_sleep_o`). +7. **R7** WFI = redirect to pc+4, then sleep until an enabled interrupt is pending (`core_sleep_o`); +8. **R8** MUL* stay 2 cycles in EX, DIV*/REM* 34, whatever the operands; IF/ID wait (no fetch), MEM/WB drain. An interrupt abandons the multiply/divide (it runs again after MRET), so the 7-cycle latency holds. Interrupt latency, counted from the cycle an enabled interrupt becomes pending to the retirement of the handler's first instruction: 5 cycles if EX holds an @@ -61,7 +64,8 @@ instruction, up to 7 if EX holds a redirect bubble or the core was asleep (rabbit3: 3 / 4). **Consequence (proven as T1):** the time between two consecutive retirements is -1, 2 or 3 cycles and depends only on those two instructions. For a straight-line +1, 2 or 3 cycles (+1 / +33 for M instructions) and depends only on those two +instructions. For a straight-line or loop path you can compute the cycle count by hand — that is what makes WCET analysis trivial for this core. @@ -74,6 +78,7 @@ Design choices you may want to change: - [ ] **All pipeline registers have an asynchronous reset** — costs area, removes X in simulation/GLS. - [ ] **`minstret` counts at EX (commit point)**, so a CSR read sees all older instructions. - [ ] Misaligned loads/stores **trap** (cause 4/6) rather than being split into two accesses. +- [ ] **M instructions wait in EX** (R8). While they wait, `ex_q` keeps the instruction but stores the *forwarded* operand values: the older instructions it forwarded from leave MEM/WB meanwhile, and the muldiv unit needs the same operands every cycle (proven: M0). Try removing those two lines and see which check fails. Things to verify yourself (good first exercises): - [ ] Draw the pipeline diagram for `lw x1,0(x2); add x3,x1,x1` and check it against a waveform (`make soc-waves CORE=rabbit5`). @@ -88,7 +93,8 @@ Things to verify yourself (good first exercises): | Memory must be zero-wait (R4); no back-pressure | M4: TDM scratchpad arbiter → stall only in MEM (Patmos rule) | | CSRs are not formally checked (riscv-formal `csrw`/`csrc_*` checks not enabled yet) | M2 | | BMC proves properties up to a depth (24 cycles timing, 12–20 riscv-formal), not unbounded | try `mode prove` (k-induction) once stable | -| No M/C extensions (software mul/div) | later; a single-cycle multiplier keeps R1 intact | +| No C extension | not planned for the RT core (code size vs. fetch simplicity) | +| A divide can be **starved** by frequent interrupts: each interrupt abandons it (up to 33 cycles lost) and it restarts after MRET; progress needs interrupts spaced more than ~34 cycles + handler time (see `../rabbit3/README.md`, M extension) | open choice: abort (now) / finish first / resume / abort once | | Register file not reset (x1..x31 start as X in gate-level sim) | fine for software that initialises registers | ## Ideas for your own properties (robotics / real time) diff --git a/rtl/cores/rabbit5/core.mk b/rtl/cores/rabbit5/core.mk index a23cf81..4ccf6ab 100644 --- a/rtl/cores/rabbit5/core.mk +++ b/rtl/cores/rabbit5/core.mk @@ -1,5 +1,5 @@ # Per-core build settings, included by the top-level and dv Makefiles. -CORE_MARCH := rv32i_zicsr +CORE_MARCH := rv32im_zicsr CORE_MABI := ilp32 # Our own RTL: no warning suppressions. CORE_VERILATOR_FLAGS := @@ -15,3 +15,14 @@ TIMING_IRQ_LATENCY := 7 # Cycles from the commit stage (EX) to retirement (WB). The timing testbench # uses it to line up its RVFI-based spec model with the core. TIMING_COMMIT_TO_RETIRE := 2 +# M extension (rule R8): cycles an instruction spends in EX, for any +# operands. FORMAL_DIV_STEPS is the divider's step count used by the +# pipeline-level proofs (a 34-cycle divide does not fit in their depth); the +# real 32 steps are proven in dv/formal/rabbit/muldiv (L1). +TIMING_MUL_CYCLES := 2 +TIMING_DIV_CYCLES := 34 +FORMAL_DIV_STEPS := 2 +# riscv-formal liveness: the check cycle (window = depth - 8). An interrupted +# divide plus a handler that starts with a divide needs a long window; +# measured: 26 passes in seconds; 22 does not finish in 25 min. +FORMAL_LIVENESS_DEPTH := 26 diff --git a/rtl/cores/rabbit5/files.f b/rtl/cores/rabbit5/files.f index 9f897ef..29662f0 100644 --- a/rtl/cores/rabbit5/files.f +++ b/rtl/cores/rabbit5/files.f @@ -1,10 +1,11 @@ -// rabbit5 (RV32I, 5-stage) + shared rabbit_common blocks + rabbit_cpu adapter. +// rabbit5 (RV32IM, 5-stage) + shared rabbit_common blocks + rabbit_cpu adapter. // ${REPO} is expanded by Verilator / the Makefiles. ${REPO}/rtl/cores/rabbit_common/rabbit_pkg.sv ${REPO}/rtl/cores/rabbit_common/rabbit_decoder.sv ${REPO}/rtl/cores/rabbit_common/rabbit_alu.sv ${REPO}/rtl/cores/rabbit_common/rabbit_regfile.sv ${REPO}/rtl/cores/rabbit_common/rabbit_csr.sv +${REPO}/rtl/cores/rabbit_common/rabbit_muldiv.sv ${REPO}/rtl/cores/rabbit_common/rabbit_execute.sv ${REPO}/rtl/cores/rabbit_common/rabbit_rvfi.sv ${REPO}/rtl/cores/rabbit5/rabbit5_core.sv diff --git a/rtl/cores/rabbit5/rabbit5_core.sv b/rtl/cores/rabbit5/rabbit5_core.sv index 003054f..6a43b6c 100644 --- a/rtl/cores/rabbit5/rabbit5_core.sv +++ b/rtl/cores/rabbit5/rabbit5_core.sv @@ -1,5 +1,5 @@ // ============================================================================= -// rabbit5_core — 5-stage in-order RV32I pipeline (single hart) +// rabbit5_core — 5-stage in-order RV32IM pipeline (single hart) // ============================================================================= // // cycle: 1 2 3 4 5 6 @@ -25,7 +25,8 @@ // R4 Memory must answer in exactly 1 cycle (grant in the request cycle, // data the next cycle). This is the scratchpad-memory assumption from // FlexPRET/Patmos; the core never waits on memory. -// R5 Nothing else ever stalls the pipeline, except WFI sleep (R7). +// R5 Nothing else ever stalls the pipeline, except WFI sleep (R7) and +// the M extension (R8). // R6 Interrupts are taken in EX, on the instruction there, which does not // retire (it runs again after MRET); IF and ID are flushed as for any // redirect, MEM and WB are older and finish. The handler's first @@ -34,10 +35,16 @@ // R7 WFI is a redirect to pc+4 (R3). If no enabled interrupt is pending, // fetch stops (core_sleep_o = 1) until one is; it restarts in the same // cycle the interrupt appears. +// R8 MUL/MULH/MULHSU/MULHU stay 2 cycles in EX, DIV/DIVU/REM/REMU 34, +// whatever the operands: they retire 1 or 33 cycles later than +// another instruction would. IF and ID wait (no fetch meanwhile); MEM +// and WB drain. An interrupt is still taken at once (R6): the +// multiply or divide is abandoned and runs again after MRET. // // So the time between two consecutive retirements is 1, 2 (R2) or 3 (R3) -// cycles and depends only on those two instructions, plus the cycles spent -// asleep, except around an interrupt (R6). +// cycles, plus 1 or 33 for M instructions (R8), and depends only on those +// two instructions, plus the cycles spent asleep, except around an +// interrupt (R6). // // Interrupts and WFI are the same as in rabbit3 (see rabbit3/README.md); only // the stage that takes them differs (EX here, X there). @@ -128,6 +135,8 @@ module rabbit5_core logic redirect; // EX changes control flow this cycle logic [31:0] redirect_pc; logic stall; // ID must wait one cycle (load-use) + logic ex_busy; // EX holds an unfinished multiply/divide (R8) + logic id_hold; // the instruction in ID stays there logic [31:0] wb_result; // final register value of the instruction in WB // =========================================================================== @@ -141,7 +150,7 @@ module rabbit5_core logic wake; // an enabled interrupt is pending logic fetch; // a fetch happens this cycle - assign fetch = fetch_enable_i && (!sleep_q || wake); + assign fetch = fetch_enable_i && (!sleep_q || wake) && !ex_busy; assign instr_req_o = fetch; assign instr_addr_o = pc_q; assign core_sleep_o = sleep_q; @@ -149,7 +158,7 @@ module rabbit5_core always_ff @(posedge clk_i or negedge rst_ni) begin if (!rst_ni) pc_q <= BOOT_ADDR; else if (redirect) pc_q <= redirect_pc; // R3 - else if (stall) pc_q <= pc_q; // R2: ask for the same word again + else if (id_hold) pc_q <= pc_q; // R2: ask for the same word again (R8: no fetch) else if (fetch) pc_q <= pc_q + 32'd4; end @@ -163,8 +172,9 @@ module rabbit5_core // =========================================================================== // ID — decode and register read // =========================================================================== - // While ID is stalled, the memory is already returning the *next* word, so - // the stalled instruction is kept in a small holding register. + // While ID waits (load-use stall, or EX busy with R8), the memory returns + // another word or none at all, so the waiting instruction is kept in a + // small holding register. logic id_valid_q; logic [31:0] id_pc_q; logic id_hold_q; @@ -182,7 +192,7 @@ module rabbit5_core end else if (redirect) begin // wrong-path instruction: drop it id_valid_q <= 1'b0; id_hold_q <= 1'b0; - end else if (stall) begin // keep the same instruction + end else if (id_hold) begin // keep the same instruction id_hold_q <= 1'b1; id_hold_instr_q <= id_instr; end else begin // take the word requested this cycle @@ -210,12 +220,20 @@ module rabbit5_core assign load_use = id_valid_q && ex_q.valid && ex_q.dec.is_load && ex_q.dec.writes_rd && ((id_dec.uses_rs1 && id_dec.rs1 == ex_q.dec.rd) || (id_dec.uses_rs2 && id_dec.rs2 == ex_q.dec.rd)); - assign stall = load_use && !redirect; // a redirect throws the ID instruction away anyway + assign stall = load_use && !redirect; // a redirect throws the ID instruction away anyway + assign id_hold = stall || ex_busy; + // While EX is busy (R8) it keeps its instruction, but takes the operand + // values it is using now: the older instructions it forwards from leave + // MEM and WB meanwhile, and the operands must not change (rabbit_execute). + logic [31:0] ex_rs1, ex_rs2; // operands after forwarding always_ff @(posedge clk_i or negedge rst_ni) begin if (!rst_ni) ex_q <= '0; else if (redirect || stall) ex_q.valid <= 1'b0; // insert a bubble - else begin + else if (ex_busy) begin + ex_q.rs1_val <= ex_rs1; + ex_q.rs2_val <= ex_rs2; + end else begin ex_q.valid <= id_valid_q; ex_q.pc <= id_pc_q; ex_q.instr <= id_instr; @@ -238,6 +256,9 @@ module rabbit5_core else return id_val; endfunction + assign ex_rs1 = forward(ex_q.dec.rs1, ex_q.rs1_val); + assign ex_rs2 = forward(ex_q.dec.rs2, ex_q.rs2_val); + exec_t ex_res; rabbit_execute #(.MTVEC_RESET(MTVEC_ADDR), .HART_ID(HART_ID)) u_execute ( .clk_i, .rst_ni, @@ -245,11 +266,12 @@ module rabbit5_core .pc_i (ex_q.pc), .instr_i (ex_q.instr), .dec_i (ex_q.dec), - .rs1_i (forward(ex_q.dec.rs1, ex_q.rs1_val)), - .rs2_i (forward(ex_q.dec.rs2, ex_q.rs2_val)), + .rs1_i (ex_rs1), + .rs2_i (ex_rs2), .res_o (ex_res), .redirect_o (redirect), .redirect_pc_o(redirect_pc), + .busy_o (ex_busy), .irq_i, .sleep_o (ex_sleep), .wake_o (wake) diff --git a/rtl/cores/rabbit5/rabbit_cpu.sv b/rtl/cores/rabbit5/rabbit_cpu.sv index f844220..33a8747 100644 --- a/rtl/cores/rabbit5/rabbit_cpu.sv +++ b/rtl/cores/rabbit5/rabbit_cpu.sv @@ -1,4 +1,4 @@ -// rabbit_cpu adapter for rabbit5 (our own 5-stage RV32I core). +// rabbit_cpu adapter for rabbit5 (our own 5-stage RV32IM core). // See rtl/cores/README.md for the port contract. rabbit5 needs memories that // grant immediately and answer one cycle later (rabbit5_core.sv, rule R4). module rabbit_cpu #( diff --git a/rtl/cores/rabbit_common/README.md b/rtl/cores/rabbit_common/README.md index e0f5b9a..e0ecba6 100644 --- a/rtl/cores/rabbit_common/README.md +++ b/rtl/cores/rabbit_common/README.md @@ -11,7 +11,8 @@ Everything an instruction *does* lives here. A rabbit core | `rabbit_alu.sv` | combinational | the ten RV32I ALU operations | | `rabbit_regfile.sv` | state | 31 × 32-bit registers (x0 = 0), 2 read ports, 1 write port, write-first bypass | | `rabbit_csr.sv` | state | machine-mode CSRs, counters, trap entry, MRET, interrupt enables (`mie`, `mip`, `mstatus.MIE`) and priority | -| `rabbit_execute.sv` | combinational + CSR state | ALU operands, branch/jump decision, exceptions, interrupts, WFI, CSR access, next pc → `exec_t` + redirect | +| `rabbit_muldiv.sv` | small state | M extension: multiply (2 cycles) and divide (34 cycles), fixed latency, abandoned on an interrupt | +| `rabbit_execute.sv` | combinational + CSR state | ALU operands, branch/jump decision, exceptions, interrupts, WFI, CSR access, M instructions (`busy_o`), next pc → `exec_t` + redirect | | `rabbit_rvfi.sv` | small state | turns the retiring `exec_t` into the RVFI port used by formal verification | ``` @@ -35,3 +36,68 @@ 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). + +## M extension (`rabbit_muldiv.sv`) + +The instruction stays in execute (the commit point) until it is done; the +pipeline holds it there while `rabbit_execute.busy_o` is 1. + +| Instructions | Cycles in execute | Depends on the operands? | +|---|---|---| +| MUL, MULH, MULHSU, MULHU | 2 | no | +| DIV, DIVU, REM, REMU | 34 (also x/0 and −2³¹/−1) | no | + +- **Multiplier:** one 33×17 signed multiplier, used twice: rs1 × low half of + rs2, then rs1 × high half of rs2 plus the first partial product (the add is + fused into the multiplier's adder tree). Both MUL and MULH* take 2 cycles. +- **Divider:** restoring long division, one quotient bit per cycle, on the + magnitudes; one adder for the steps and one negator shared by the first + cycle (|rs1|) and the last (sign of the result). No early exit: robot + control code needs the worst case to be the normal case. +- **Interrupts** are not delayed by a divide: the divide is abandoned and runs + again after MRET (the proven interrupt latency stays 4 / 7 cycles). The + price: each interrupt that hits a divide throws away up to 33 cycles, and + interrupts that keep coming faster than ~34 cycles + handler time **starve** + the divide (no progress guarantee). See the known limitation in + `../rabbit3/README.md`. + +### Why this design (measured on sky130, Yosys `synth -booth` + ABC, typical corner) + +Combinational parts alone (delays without wires, for comparison only): + +| Part | Area µm² | Delay | +|---|---|---| +| 32-bit adder (for scale) | 1 506 | 3.1 ns | +| full 33×33 multiplier (all of MUL/MULH* in one cycle) | 31 734 | 7.4 ns | +| **33×17 multiplier + fused add (ours)** | **20 366** | 6.9 ns | +| 17×17 multiply-add (Ibex "fast" style: MUL 3, MULH 4 cycles) | 11 549 | 5.3 ns | +| same full 33×33 without `-booth` | 47 405 | 7.8 ns | + +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** | +| 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 | + +- 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` / + `mcycle` counters (cheap to fix later by registering that enable). ABC's + delay varies by about ±0.6 ns between runs of nearly identical RTL, hence + the ranges; a real answer needs OpenROAD with wires — a later step. +- **Operand isolation** (power): unless an M instruction is in execute, the + multiplier and the divider's negator see zeros, so they do not switch on + the operands of every other instruction. Cost: ~100 µm² (0.1 %). +- `synth -booth` saves 25–33 % of multiplier area: use it for every real + synthesis run. +- Half of each core's area is flip-flops (mostly the register file), so the + M unit looks large next to the logic. It is the obvious place to save area + later: the divider could reuse the multiplier's partial-product register, + and the 33×17 multiplier could become the int8 dot-product unit (next step). + +Verification: `dv/formal/rabbit/muldiv/` (values for every input at 4, 6 and +8 bits, exact latency at 32 bits), riscv-formal with ALTOPS for the pipeline, +`sw/baremetal/muldiv` on every core. diff --git a/rtl/cores/rabbit_common/rabbit_decoder.sv b/rtl/cores/rabbit_common/rabbit_decoder.sv index f0b320d..645caf0 100644 --- a/rtl/cores/rabbit_common/rabbit_decoder.sv +++ b/rtl/cores/rabbit_common/rabbit_decoder.sv @@ -1,7 +1,7 @@ // ============================================================================= // rabbit_decoder — instruction bits -> decoded_t (pure combinational) // ============================================================================= -// Supported: all of RV32I, plus FENCE (a no-op) and WFI, +// Supported: all of RV32I and RV32M, plus FENCE (a no-op) and WFI, // ECALL, EBREAK, MRET and the six Zicsr instructions. // Anything else sets `illegal`; the EX stage turns that into a trap. // ============================================================================= @@ -134,8 +134,11 @@ module rabbit_decoder 3'b111: dec_o.alu_op = ALU_AND; default: ; endcase + // M extension (funct7 = 0000001): all eight funct3 values exist + if (funct7 == FUNCT7_MULDIV) + dec_o.is_muldiv = 1'b1; // only ADD/SUB and SRL/SRA have a second encoding (funct7 = 0100000) - if (funct7 == 7'b010_0000) + else if (funct7 == 7'b010_0000) dec_o.illegal = (funct3 != 3'b000) && (funct3 != 3'b101); else dec_o.illegal = (funct7 != 7'b000_0000); @@ -193,6 +196,7 @@ module rabbit_decoder dec_o.is_ebreak = 1'b0; dec_o.is_mret = 1'b0; dec_o.is_wfi = 1'b0; + dec_o.is_muldiv = 1'b0; end end diff --git a/rtl/cores/rabbit_common/rabbit_execute.sv b/rtl/cores/rabbit_common/rabbit_execute.sv index 9ec6041..eb51652 100644 --- a/rtl/cores/rabbit_common/rabbit_execute.sv +++ b/rtl/cores/rabbit_common/rabbit_execute.sv @@ -22,9 +22,17 @@ // asks the pipeline to sleep (sleep_o) unless an enabled interrupt is // already pending. The pipeline stops fetching until wake_o. // +// M extension (rabbit_muldiv): a multiply takes 2 cycles in execute, a +// divide 34, whatever the operands. Until it is done, busy_o = 1: the +// pipeline must keep the instruction here, with the same operand values, +// and let nothing younger move. An interrupt ends the wait at once: the +// multiply/divide is abandoned and runs again after MRET, so the interrupt +// latency does not grow. +// // operands ─► ALU ─────────────► result / load-store address // └─► branch unit ─────► taken? target? // └─► CSR unit ────────► old CSR value, trap entry, MRET +// └─► rabbit_muldiv ───► product / quotient (2 or 34 cycles) // └─► exception check ─► trap? cause? // └► next_pc, redirect // ============================================================================= @@ -47,6 +55,7 @@ module rabbit_execute output exec_t res_o, output logic redirect_o, // control flow changes: fetch from redirect_pc_o output logic [31:0] redirect_pc_o, + output logic busy_o, // M instruction not finished: hold it in execute input logic [31:0] irq_i, // interrupt request lines (see rabbit_pkg) output logic sleep_o, // WFI executed: stop fetching ... @@ -59,11 +68,12 @@ module rabbit_execute assign irq_take = valid_i && irq_pending; // RVFI: the next instruction that executes is the first one of the handler + // (cleared when an instruction leaves execute: an M instruction may wait) logic intr_next_q; always_ff @(posedge clk_i or negedge rst_ni) begin - if (!rst_ni) intr_next_q <= 1'b0; - else if (irq_take) intr_next_q <= 1'b1; - else if (valid_i) intr_next_q <= 1'b0; + if (!rst_ni) intr_next_q <= 1'b0; + else if (irq_take) intr_next_q <= 1'b1; + else if (valid_i && !busy_o) intr_next_q <= 1'b0; end @@ -113,6 +123,67 @@ module rabbit_execute trap = trap && valid_i; end + // ---- M extension --------------------------------------------------------------- + logic md_req, md_done; + logic [31:0] md_result; + assign md_req = valid_i && dec_i.is_muldiv && !irq_pending; + assign busy_o = md_req && !md_done; + +`ifdef RABBIT_DIV_STEPS + localparam int unsigned DIV_STEPS = `RABBIT_DIV_STEPS; // formal only, see rabbit_muldiv +`else + localparam int unsigned DIV_STEPS = 32; +`endif + + logic [31:0] md_value; + rabbit_muldiv #(.W(32), .DIV_STEPS(DIV_STEPS)) u_muldiv ( + .clk_i, .rst_ni, + .en_i (valid_i && dec_i.is_muldiv), + .req_i (md_req), + .op_i (dec_i.funct3), + .a_i (rs1_i), + .b_i (rs2_i), + .done_o (md_done), + .result_o(md_value) + ); + +`ifdef RISCV_FORMAL_ALTOPS + // riscv-formal cannot reason about real multiplication and division; with + // ALTOPS it expects these stand-in results instead (same timing). The real + // arithmetic is proven separately: dv/formal/rabbit/muldiv. + always_comb begin + unique case (dec_i.funct3) + 3'd0: md_result = (rs1_i + rs2_i) ^ 32'h5876_063e; // MUL + 3'd1: md_result = (rs1_i + rs2_i) ^ 32'hf658_3fb7; // MULH + 3'd2: md_result = (rs1_i - rs2_i) ^ 32'hecfb_e137; // MULHSU + 3'd3: md_result = (rs1_i + rs2_i) ^ 32'h949c_e5e8; // MULHU + 3'd4: md_result = (rs1_i - rs2_i) ^ 32'h7f85_29ec; // DIV + 3'd5: md_result = (rs1_i - rs2_i) ^ 32'h10e8_fd70; // DIVU + 3'd6: md_result = (rs1_i - rs2_i) ^ 32'h8da6_8fa5; // REM + default: md_result = (rs1_i - rs2_i) ^ 32'h3138_d0e1; // REMU + endcase + end + logic unused_md; + assign unused_md = ^md_value; +`else + assign md_result = md_value; +`endif + +`ifndef SYNTHESIS + // The contract with the pipeline: the operands do not change while an M + // instruction is held here (also proven in dv/formal/rabbit/timing, M0). + logic busy_q; + logic [31:0] rs1_q, rs2_q; + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) busy_q <= 1'b0; + else begin + busy_q <= busy_o; rs1_q <= rs1_i; rs2_q <= rs2_i; + if (busy_q && md_req && (rs1_i != rs1_q || rs2_i != rs2_q)) + $error("rabbit_execute: operands changed while a multiply/divide was held"); + end + end +`endif + // ---- CSRs ------------------------------------------------------------------- logic [31:0] csr_rdata, mtvec, mepc; logic csr_write_req; @@ -133,7 +204,7 @@ module rabbit_execute .trap_pc_i (pc_i), .trap_tval_i (trap_tval), .mret_i (valid_i && dec_i.is_mret && !trap), - .instret_i (valid_i && !trap), + .instret_i (valid_i && !trap && !busy_o), .irq_i, .irq_wake_o (wake_o), .irq_pending_o(irq_pending), @@ -159,7 +230,7 @@ module rabbit_execute // ---- the result record ------------------------------------------------------------ always_comb begin res_o = '0; - res_o.valid = valid_i && !irq_take; // an interrupted instruction never retires + res_o.valid = valid_i && !irq_take && !busy_o; // interrupted / not finished: no res_o.pc = pc_i; res_o.instr = instr_i; res_o.next_pc = next_pc; @@ -170,7 +241,7 @@ module rabbit_execute unique case (dec_i.res) RES_PC4: res_o.result = pc_i + 32'd4; RES_CSR: res_o.result = csr_rdata; - default: res_o.result = alu_y; + default: res_o.result = dec_i.is_muldiv ? md_result : alu_y; endcase res_o.is_load = dec_i.is_load && !trap; res_o.is_store = dec_i.is_store && !trap; diff --git a/rtl/cores/rabbit_common/rabbit_muldiv.sv b/rtl/cores/rabbit_common/rabbit_muldiv.sv new file mode 100644 index 0000000..2ef9da1 --- /dev/null +++ b/rtl/cores/rabbit_common/rabbit_muldiv.sv @@ -0,0 +1,180 @@ +// ============================================================================= +// rabbit_muldiv — RISC-V M extension: multiply and divide, fixed latency +// ============================================================================= +// Used by rabbit_execute. The instruction stays in execute (the commit point) +// until done_o; the pipeline holds it there (rabbit_execute.busy_o). +// +// LATENCY never depends on the operand values (robot control loops need a +// worst case that is also the normal case, and the timing proof needs it): +// +// MUL, MULH, MULHSU, MULHU 2 cycles in execute (MUL_CYCLES) +// DIV, DIVU, REM, REMU W+2 cycles = 34 (DIV_CYCLES) +// (also for x/0 and the -2^31/-1 overflow) +// +// MULTIPLIER — one (W+1) x (H+1) signed multiplier, used twice (H = W/2): +// +// A = rs1, sign- or zero-extended to W+1 bits +// B = B_hi * 2^H + B_lo B_lo = rs2[H-1:0] (always unsigned) +// B_hi = rs2[W-1:H] (signed for MUL/MULH) +// cycle 1: P0 = A * B_lo -> register p0_q +// cycle 2: P1 = A * B_hi + (P0 >>> H) (the add is fused into the +// multiplier's adder tree) +// A * B = {P1, P0[H-1:0]} MUL = low W bits, MULH* = high W bits +// +// Why this size: a full 33x33 multiplier is 1.75x the area and its delay +// would be the core's longest path; Ibex' 17x17 MAC needs 3-4 cycles. +// Measured on sky130 in docs: rtl/cores/rabbit_common/README.md. +// +// DIVIDER — restoring long division on the magnitudes, one bit per cycle: +// +// cycle 1 : quo = |rs1|, rem = 0, keep rs2 and the signs +// cycles 2..W+1 : {rem, quo} <<= 1; if rem >= |rs2|: rem -= |rs2|, quo[0] = 1 +// cycle W+2 : apply the signs, result out (done_o) +// +// x/0 needs no special path: every subtraction of 0 succeeds, so the +// quotient is all ones and the remainder is x, exactly what RISC-V asks for +// (only the sign fix-up of the quotient is skipped for x/0). +// -2^31 / -1 needs none either: |x| = 2^31 fits in W unsigned bits, and the +// quotient 2^31 reinterpreted as signed is -2^31, as required. +// +// POWER (operand isolation): the multiplier and the negator see zeros unless +// an M instruction is in execute (en_i). Without this, the 33x17 multiplier +// would switch on the operands of every ADD, load, branch ... for nothing. +// en_i comes from decode only (not from the interrupt logic), so no path from +// the interrupt inputs runs through the multiplier. +// +// INTERRUPTS: if req_i drops before done_o (the instruction was interrupted), +// the unit forgets everything and is idle again in the next cycle. The +// instruction runs again from the start after MRET. +// +// The operands a_i / b_i must stay the same while the instruction is held in +// execute (both cores guarantee that). +// +// W is a parameter only so that dv/formal/rabbit/muldiv can prove the very +// same RTL correct for EVERY input at a small width (W = 8); the cores use 32. +// ============================================================================= +module rabbit_muldiv #( + parameter int unsigned W = 32, + // Division steps. Must be W for correct quotients. The pipeline-level + // proofs (riscv-formal with ALTOPS, timing) use a smaller value so that a + // divide fits in their proof depth: there the pipeline only sees done_o, + // and the value is replaced anyway. The unit proof checks the real one. + parameter int unsigned DIV_STEPS = W +) ( + input logic clk_i, + input logic rst_ni, + + input logic en_i, // an M instruction is in execute (power gating only) + input logic req_i, // ... and is not being interrupted: work on it + input logic [2:0] op_i, // funct3: 0 MUL 1 MULH 2 MULHSU 3 MULHU 4 DIV 5 DIVU 6 REM 7 REMU + input logic [W-1:0] a_i, // rs1 + input logic [W-1:0] b_i, // rs2 + output logic done_o, // result_o is valid; the instruction may leave execute + output logic [W-1:0] result_o +); + localparam int unsigned H = W / 2; + localparam int unsigned P = W + H + 2; // width of one partial product + localparam int unsigned DIV_CYCLES = DIV_STEPS + 2; + localparam int unsigned CW = $clog2(DIV_CYCLES); + + // ---- control: one cycle counter for both ------------------------------------ + // cnt_q = how many cycles this instruction has already spent in the unit + logic [CW-1:0] cnt_q; + logic is_div, first; + assign is_div = op_i[2]; + assign first = (cnt_q == '0); + assign done_o = req_i && (is_div ? (cnt_q == CW'(DIV_CYCLES - 1)) : (cnt_q == CW'(1))); + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) cnt_q <= '0; + else if (!req_i || done_o) cnt_q <= '0; // finished or interrupted + else cnt_q <= cnt_q + 1'b1; + end + + // ---- multiplier -------------------------------------------------------------- + logic a_signed, b_signed; + assign a_signed = (op_i[1:0] != 2'b11); // MUL, MULH, MULHSU + assign b_signed = !op_i[1]; // MUL, MULH + + logic signed [W:0] mul_a; + logic signed [H:0] mul_b; + logic signed [P-1:0] mul_c, mul_y; + logic [P-1:0] p0_q; + + logic mul_on, div_on; // operand isolation (POWER) + assign mul_on = en_i && !is_div; + assign div_on = en_i && is_div; + + assign mul_a = mul_on ? {a_signed && a_i[W-1], a_i} : '0; + assign mul_b = !mul_on ? '0 + : first ? {1'b0, b_i[H-1:0]} : {b_signed && b_i[W-1], b_i[W-1:H]}; + assign mul_c = first ? '0 : P'($signed(p0_q) >>> H); + assign mul_y = mul_a * mul_b + mul_c; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) p0_q <= '0; + else if (req_i && !is_div && first) p0_q <= mul_y; + end + + logic [2*W-1:0] product; + assign product = {mul_y[W+H-1:0], p0_q[H-1:0]}; // the full 2W-bit product (cycle 2) + + // ---- divider ------------------------------------------------------------------- + // Area: one W+1-bit adder for the steps, and ONE negator shared by the first + // cycle (|rs1|) and the last (sign of the result). The divisor is kept as + // it is; "rem - |div|" becomes "rem + div" when the divisor is negative. + logic [W-1:0] rem_q, quo_q, div_q; + logic div_neg_q, quo_neg_q, rem_neg_q; + logic div_signed, a_neg, b_neg; + logic [W:0] rem_shift, rem_try; + + assign div_signed = !op_i[0]; // DIV, REM + assign a_neg = div_signed && a_i[W-1]; + assign b_neg = div_signed && b_i[W-1]; + + // rem_try = rem_shift - |div| (rem_try[W] = 1: the divisor does not fit) + assign rem_shift = {rem_q, quo_q[W-1]}; + assign rem_try = div_neg_q ? rem_shift + {1'b1, div_q} + : rem_shift - {1'b0, div_q}; + + // the shared negator: |rs1| in the first cycle, the signed result in the last + logic want_rem; + logic [W-1:0] neg_in, neg_out; + assign want_rem = op_i[1]; // REM, REMU + assign neg_in = !div_on ? '0 : first ? a_i : (want_rem ? rem_q : quo_q); + assign neg_out = -neg_in; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + rem_q <= '0; quo_q <= '0; div_q <= '0; + div_neg_q <= 1'b0; quo_neg_q <= 1'b0; rem_neg_q <= 1'b0; + end else if (req_i && is_div) begin + if (first) begin + rem_q <= '0; + quo_q <= a_neg ? neg_out : a_i; // |rs1| + div_q <= b_i; + div_neg_q <= b_neg; + quo_neg_q <= (a_neg != b_neg) && (b_i != '0); // x/0 = all ones, unsigned + rem_neg_q <= a_neg; // remainder has the dividend's sign + end else if (!done_o) begin + rem_q <= rem_try[W] ? rem_shift[W-1:0] : rem_try[W-1:0]; + quo_q <= {quo_q[W-2:0], !rem_try[W]}; + end + end + end + + logic [W-1:0] div_result; + assign div_result = (want_rem ? rem_neg_q : quo_neg_q) ? neg_out + : (want_rem ? rem_q : quo_q); + + // ---- result ---------------------------------------------------------------------- + always_comb begin + unique case (op_i) + 3'd0: result_o = product[W-1:0]; // MUL + 3'd1, 3'd2, + 3'd3: result_o = product[2*W-1:W]; // MULH, MULHSU, MULHU + default: result_o = div_result; // DIV, DIVU, REM, REMU + endcase + end + +endmodule diff --git a/rtl/cores/rabbit_common/rabbit_pkg.sv b/rtl/cores/rabbit_common/rabbit_pkg.sv index 33756b4..9f089df 100644 --- a/rtl/cores/rabbit_common/rabbit_pkg.sv +++ b/rtl/cores/rabbit_common/rabbit_pkg.sv @@ -23,6 +23,9 @@ package rabbit_pkg; localparam logic [6:0] OPC_JAL = 7'b110_1111; localparam logic [6:0] OPC_SYSTEM = 7'b111_0011; // ECALL, EBREAK, MRET, WFI, CSR* + // funct7 of OPC_OP that selects the M extension (MUL..REMU) + localparam logic [6:0] FUNCT7_MULDIV = 7'b000_0001; + // --------------------------------------------------------------------------- // ALU operations // --------------------------------------------------------------------------- @@ -72,6 +75,7 @@ package rabbit_pkg; logic is_ebreak; logic is_mret; logic is_wfi; + logic is_muldiv; // M extension: MUL* / DIV* / REM* (funct3 says which) } decoded_t; // --------------------------------------------------------------------------- @@ -92,8 +96,8 @@ package rabbit_pkg; localparam logic [11:0] CSR_MINSTRETH= 12'hB82; localparam logic [11:0] CSR_MHARTID = 12'hF14; - // misa: MXL=1 (32-bit), extension I only - localparam logic [31:0] MISA_VALUE = 32'h4000_0100; + // misa: MXL=1 (32-bit), extensions I and M + localparam logic [31:0] MISA_VALUE = 32'h4000_1100; // --------------------------------------------------------------------------- // Interrupts. Line i of irq_i is bit i of mip and mie (RISC-V standard diff --git a/sw/baremetal/muldiv/main.c b/sw/baremetal/muldiv/main.c new file mode 100644 index 0000000..7bfebe1 --- /dev/null +++ b/sw/baremetal/muldiv/main.c @@ -0,0 +1,216 @@ +/* M-extension self-test for the rabbit SoC (runs on every core; CV32E40P is + * the reference). + * + * 1. corner cases of all eight instructions (x/0, -2^31/-1, signs, ...) + * 2. pseudo-random operands, checked against a software model that uses + * only shifts and adds (no MUL/DIV instructions) + * 3. timing: cycles per MUL / DIV, and that they do not depend on the + * operands (rabbit cores only: CV32E40P's divider is data-dependent) + * 4. an interrupt in the middle of a divide is taken at once, and the + * divide still gives the right result afterwards + * + * Returns the number of failed checks (0 = PASS). + */ +#include "rabbit_sim.h" + +static int failures; + +static void fail(const char *what, uint32_t a, uint32_t b, uint32_t got, uint32_t exp) { + if (failures < 10) { + sim_puts(" [FAIL] "); sim_puts(what); + sim_puts(" a="); sim_puthex(a); sim_puts(" b="); sim_puthex(b); + sim_puts(" got="); sim_puthex(got); sim_puts(" expected="); sim_puthex(exp); + sim_putc('\n'); + } + failures++; +} + +static void check(const char *name, uint32_t got, uint32_t expected) { + sim_puts(got == expected ? " [ok] " : " [FAIL] "); + sim_puts(name); + sim_puts(" = "); + sim_puthex(got); + if (got != expected) { + sim_puts(" expected "); + sim_puthex(expected); + failures++; + } + sim_putc('\n'); +} + +/* ---- the eight instructions, exactly as written (no compiler tricks) ---- */ +#define OP(name) \ + static inline uint32_t op_##name(uint32_t a, uint32_t b) { \ + uint32_t r; __asm__ volatile(#name " %0, %1, %2" : "=r"(r) : "r"(a), "r"(b)); return r; } +OP(mul) OP(mulh) OP(mulhsu) OP(mulhu) OP(div) OP(divu) OP(rem) OP(remu) + +/* ---- software model: shifts and adds only -------------------------------- */ +static uint64_t umul64(uint32_t a, uint32_t b) { + uint64_t acc = 0, x = a; + while (b) { + if (b & 1u) acc += x; + x <<= 1; + b >>= 1; + } + return acc; +} +static uint32_t neg(uint32_t x) { return ~x + 1u; } +static uint32_t abs32(uint32_t x) { return (x >> 31) ? neg(x) : x; } + +/* high word of a*b with a and/or b read as signed: fix up the unsigned one */ +static uint32_t model_mulh(uint32_t a, uint32_t b, int a_signed, int b_signed) { + uint32_t hi = (uint32_t)(umul64(a, b) >> 32); + if (a_signed && (a >> 31)) hi -= b; + if (b_signed && (b >> 31)) hi -= a; + return hi; +} + +static void udivmod(uint32_t a, uint32_t b, uint32_t *q, uint32_t *r) { + if (b == 0) { *q = 0xffffffffu; *r = a; return; } + uint32_t quo = 0, rem = 0; + for (int i = 31; i >= 0; i--) { + rem = (rem << 1) | ((a >> i) & 1u); + if (rem >= b) { rem -= b; quo |= 1u << i; } + } + *q = quo; *r = rem; +} + +static uint32_t model(int op, uint32_t a, uint32_t b) { + uint32_t q, r; + switch (op) { + case 0: return (uint32_t)umul64(a, b); + case 1: return model_mulh(a, b, 1, 1); + case 2: return model_mulh(a, b, 1, 0); + case 3: return model_mulh(a, b, 0, 0); + case 4: case 6: /* DIV, REM */ + if (b == 0) return op == 4 ? 0xffffffffu : a; + if (a == 0x80000000u && b == 0xffffffffu) return op == 4 ? a : 0; + udivmod(abs32(a), abs32(b), &q, &r); + if (op == 4) return ((a ^ b) >> 31) ? neg(q) : q; + return (a >> 31) ? neg(r) : r; + case 5: udivmod(a, b, &q, &r); return q; + default: udivmod(a, b, &q, &r); return r; + } +} + +static uint32_t hw(int op, uint32_t a, uint32_t b) { + switch (op) { + case 0: return op_mul(a, b); + case 1: return op_mulh(a, b); + case 2: return op_mulhsu(a, b); + case 3: return op_mulhu(a, b); + case 4: return op_div(a, b); + case 5: return op_divu(a, b); + case 6: return op_rem(a, b); + default: return op_remu(a, 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 */ +#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)); \ + (void)r; return t1 - t0; } +TIMED(add) TIMED(mul) TIMED(mulhu) TIMED(div) TIMED(remu) + +/* ---- interrupt during a divide ---------------------------------------------- */ +static volatile uint32_t n_irq, entry_cycle; + +void __attribute__((interrupt("machine"))) trap_entry(void) { + uint32_t now = sim_cycles(); + uint32_t cause = CSR_READ(mcause); + if (!(cause & MCAUSE_IRQ)) { /* an exception: stop the test */ + REG32(RABBIT_SIM_EXIT) = 0xDEAD0000u | (cause & 0x3ff); + for (;;) { } + } + entry_cycle = now; + n_irq++; + sim_irq_clear(1u << (cause & 0x1f)); +} + +static uint32_t xs = 0x2545F491u; /* xorshift32 */ +static uint32_t rnd(void) { xs ^= xs << 13; xs ^= xs >> 17; xs ^= xs << 5; return xs; } + +int main(void) { + sim_puts("\nrt-rabbit: M extension test\n"); + irq_global_disable(); + CSR_WRITE(mie, 0); + + /* 1. corner cases --------------------------------------------------------- */ + static const uint32_t v[] = {0, 1, 7, 0x7fffffffu, 0x80000000u, 0x80000001u, + 0xfffffffeu, 0xffffffffu, 0x0000ffffu, 0xdeadbeefu}; + const int nv = sizeof v / sizeof v[0]; + int before = failures; + for (int op = 0; op < 8; op++) + for (int i = 0; i < nv; i++) + for (int j = 0; j < nv; j++) { + uint32_t got = hw(op, v[i], v[j]), exp = model(op, v[i], v[j]); + if (got != exp) fail(names[op], v[i], v[j], got, exp); + } + check("corner cases (8 ops x 10 x 10) failures", failures - before, 0); + check(" div -2^31 / -1", op_div(0x80000000u, 0xffffffffu), 0x80000000u); + check(" rem -2^31 % -1", op_rem(0x80000000u, 0xffffffffu), 0); + check(" div -7 / 0 ", op_div(neg(7), 0), 0xffffffffu); + check(" rem -7 % 0 ", op_rem(neg(7), 0), neg(7)); + check(" divu 7 / 0 ", op_divu(7, 0), 0xffffffffu); + check(" mulhsu -1 * max", op_mulhsu(0xffffffffu, 0xffffffffu), 0xffffffffu); + + /* 2. random operands ------------------------------------------------------- */ + before = failures; + for (int n = 0; n < 48; n++) { + uint32_t a = rnd(), b = rnd(); + if (n & 1) b >>= (rnd() & 31); /* small divisors too */ + for (int op = 0; op < 8; op++) { + uint32_t got = hw(op, a, b), exp = model(op, a, b); + if (got != exp) fail(names[op], a, b, got, exp); + } + } + check("random (48 x 8 ops) failures ", failures - before, 0); + + /* 3. timing ------------------------------------------------------------------ */ + uint32_t base = time_add(1, 2); + uint32_t t_mul = time_mul(3, 5) - base, t_div = time_div(100, 7) - base; + sim_puts(" extra cycles: mul = "); sim_puthex(t_mul); + sim_puts(" mulhu = "); sim_puthex(time_mulhu(0xffffffffu, 0xffffffffu) - base); + sim_puts(" div = "); sim_puthex(t_div); + sim_putc('\n'); + int rabbit = !(CSR_READ(misa) & (1u << 2)); /* CV32E40P has C; its divider is data-dependent */ + if (rabbit) { + static const uint32_t da[] = {0, 1, 0x80000000u, 0xffffffffu, 12345}; + static const uint32_t db[] = {0, 1, 0xffffffffu, 0x80000000u, 3}; + uint32_t same_div = 1, same_mul = 1; + for (int i = 0; i < 5; i++) + for (int j = 0; j < 5; j++) { + same_div &= (time_div(da[i], db[j]) - base == t_div); + same_div &= (time_remu(da[i], db[j]) - base == t_div); + same_mul &= (time_mul(da[i], db[j]) - base == t_mul); + same_mul &= (time_mulhu(da[i], db[j]) - base == t_mul); + } + check("mul time independent of data ", same_mul, 1); + check("div time independent of data ", same_div, 1); + } + + /* 4. interrupt in the middle of a divide ------------------------------------ */ + n_irq = 0; + CSR_WRITE(mie, 1u << IRQ_FAST(0)); + irq_global_enable(); + uint32_t a = 1000000007u, b = 97u, q; + uint32_t t0 = sim_cycles(); + __asm__ volatile( + "sw %[m], 0(%[irq])\n\t" /* raise line 16 ... */ + "divu %[q], %[a], %[b]\n\t" /* ... while this divide runs */ + : [q] "=&r"(q) + : [m] "r"(1u << IRQ_FAST(0)), [irq] "r"(RABBIT_SIM_IRQ), [a] "r"(a), [b] "r"(b) + : "memory"); + irq_global_disable(); + check("irq taken during divide ", n_irq, 1); + check(" divide result after MRET ", q, 10309278u); + sim_puts(" raise -> handler (cycles) = "); sim_puthex(entry_cycle - t0); sim_putc('\n'); + + sim_puts(failures ? "RESULT: FAIL\n" : "RESULT: PASS\n"); + return failures; +} diff --git a/tools/abc_sky130.scr b/tools/abc_sky130.scr new file mode 100644 index 0000000..2583479 --- /dev/null +++ b/tools/abc_sky130.scr @@ -0,0 +1,7 @@ +strash +dch -f +map -D 1000 +buffer +upsize -D 1000 +dnsize -D 1000 +stime -p diff --git a/tools/check_all.sh b/tools/check_all.sh new file mode 100755 index 0000000..d3a2847 --- /dev/null +++ b/tools/check_all.sh @@ -0,0 +1,92 @@ +#!/usr/bin/env bash +# 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 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) +# tools/check_all.sh mutants plant known bugs, check they are caught (~30-60 min) +# tools/check_all.sh all everything above (~2-3 h) +# +# Several stages can be given: tools/check_all.sh quick formal +# Logs: build/check_all//... Summary at the end; exit code 1 if anything failed. +# +# Needs (as in CI): verilator >= 5.03x, yosys with the slang frontend, sby + +# boolector + yosys-abc (OSS CAD Suite has all of them), riscv64-unknown-elf-gcc, +# uv. "synth" also needs the sky130 PDK (see tools/synth_sky130.sh). +set -uo pipefail +REPO=$(cd "$(dirname "$0")/.." && pwd) +cd "$REPO" + +STAGES=${*:-quick gls} +[ "$STAGES" = all ] && STAGES="quick gls formal synth mutants" +LOGS=build/check_all +mkdir -p "$LOGS" +SUMMARY=() +FAILED=0 + +need() { command -v "$1" >/dev/null || { echo "missing tool: $1"; exit 1; }; } +need make; need verilator; need yosys; need uv; need riscv64-unknown-elf-gcc +case " $STAGES " in *" formal "*|*" mutants "*) need sby; need yosys-abc ;; esac + +# step +step() { + local name=$1 expect=$2; shift 2 + local log="$LOGS/$name.log" t0=$SECONDS + mkdir -p "$(dirname "$log")" + printf '%-36s ' "$name" + if "$@" > "$log" 2>&1 && { [ -z "$expect" ] || grep -q "$expect" "$log"; }; then + local extra; extra=$(grep -oE 'finished after [0-9]+ cycles|[0-9]+/[0-9]+ checks PASS' "$log" | tail -1) + printf 'PASS %5ds %s\n' $((SECONDS - t0)) "$extra" + SUMMARY+=("PASS $name $extra") + else + printf 'FAIL %5ds see %s\n' $((SECONDS - t0)) "$log" + SUMMARY+=("FAIL $name ($log)") + FAILED=1 + fi +} + +for stage in $STAGES; do + echo "=== $stage" + case $stage in + quick) + for c in rabbit3 rabbit5 cv32e40p; 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 + done + done + step "quick/muldiv-exhaustive-8bit" "RESULT: PASS" make -C dv/formal/rabbit muldiv-sim + ;; + gls) + for c in rabbit3 rabbit5; do + for p in hello irq muldiv; do + step "gls/$c-$p" "RESULT: PASS" make gls-smoke CORE=$c PROG=$p + done + done + ;; + formal) + step "formal/muldiv-unit" "" make -C dv/formal/rabbit muldiv + for c in rabbit5 rabbit3; do + step "formal/$c-riscv-formal" "53/53 checks PASS" make -C dv/formal/rabbit CORE=$c riscv-formal + step "formal/$c-timing" "" make -C dv/formal/rabbit CORE=$c timing + done + ;; + synth) + step "synth/sky130" "" tools/synth_sky130.sh + cat "$LOGS/synth/sky130.log" + ;; + mutants) + step "mutants/all" "" python3 tools/mutants.py --baseline + tail -12 "$LOGS/mutants/all.log" + ;; + *) echo "unknown stage: $stage"; exit 2 ;; + esac +done + +echo +echo "=== summary ($STAGES)" +printf '%s\n' "${SUMMARY[@]}" +[ $FAILED = 0 ] && echo "ALL PASS" || echo "SOME CHECKS FAILED" +exit $FAILED diff --git a/tools/mutants.py b/tools/mutants.py new file mode 100755 index 0000000..c934489 --- /dev/null +++ b/tools/mutants.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Mutation tests: plant a known bug, check that verification catches it. + +A check that never fails proves nothing. Each mutant below changes one line +of RTL in a throw-away copy of the repository (build/mutants//) and runs +the check that should catch it. The mutant is CAUGHT if that check fails. +The original tree is only read, never modified. + + tools/mutants.py all mutants (about 30-60 min) + tools/mutants.py --list show them + tools/mutants.py div0-sign r5-no-operand-refresh selected ones + tools/mutants.py --baseline also run each check on the unmodified copy + (it must PASS there, otherwise "caught" + would mean nothing) +""" +import argparse +import shutil +import subprocess +import sys +import time +from pathlib import Path + +REPO = Path(__file__).resolve().parent.parent +WORK = REPO / "build" / "mutants" + +MULDIV = "rtl/cores/rabbit_common/rabbit_muldiv.sv" +EXECUTE = "rtl/cores/rabbit_common/rabbit_execute.sv" +R3 = "rtl/cores/rabbit3/rabbit3_core.sv" +R5 = "rtl/cores/rabbit5/rabbit5_core.sv" + + +def sby(task): + """One task of the muldiv unit proof (exit code != 0 on FAIL).""" + return {"cmd": ["sby", "-f", "muldiv.sby", task], "cwd": "dv/formal/rabbit/muldiv"} + + +def rvf(core, check): + """One riscv-formal check; the verdict is read from its status file.""" + return { + "cmd": ["make", f"CORE={core}", "check", f"C={check}"], + "cwd": "dv/formal/rabbit", + "status": f"dv/formal/rabbit/build/{core}/riscv-formal/cores/{core}/checks/{check}/status", + } + + +MUTANTS = [ + # --- multiply/divide unit (seconds each) ----------------------------------- + dict(name="div0-sign", what="x/0: quotient sign fix-up not skipped", + file=MULDIV, old="(a_neg != b_neg) && (b_i != '0)", new="(a_neg != b_neg)", + check=sby("prove4")), + dict(name="mulh-rs2-unsigned", what="MULH ignores the sign of rs2", + file=MULDIV, old="assign b_signed = !op_i[1];", new="assign b_signed = 1'b0;", + check=sby("bmc6")), + dict(name="no-restart", what="an interrupted instruction does not restart", + file=MULDIV, old="else if (!req_i || done_o) cnt_q <= '0;", + new="else if (done_o) cnt_q <= '0;", check=sby("prove4")), + dict(name="div-one-longer", what="divide takes one cycle more than declared", + file=MULDIV, old="localparam int unsigned DIV_CYCLES = DIV_STEPS + 2;", + new="localparam int unsigned DIV_CYCLES = DIV_STEPS + 3;", check=sby("lat32")), + # --- pipelines (one riscv-formal check each, 1-15 min) ---------------------- + dict(name="intr-flag-lost", what="rvfi_intr cleared while an M instruction waits (the real bug found)", + file=EXECUTE, old="else if (valid_i && !busy_o) intr_next_q <= 1'b0;", + new="else if (valid_i) intr_next_q <= 1'b0;", check=rvf("rabbit5", "pc_fwd_ch0")), + dict(name="r5-no-operand-refresh", what="rabbit5: EX does not keep the forwarded operands while it waits", + file=R5, old=" ex_q.rs1_val <= ex_rs1;\n ex_q.rs2_val <= ex_rs2;\n", new="", + check=rvf("rabbit5", "reg_ch0")), + dict(name="r3-fetch-while-busy", what="rabbit3: fetch continues while X waits", + file=R3, old="assign fetch = fetch_enable_i && (!sleep_q || wake) && !x_busy;", + new="assign fetch = fetch_enable_i && (!sleep_q || wake);", + check=rvf("rabbit3", "pc_fwd_ch0")), + dict(name="r3-no-hold-register", what="rabbit3: no instruction holding register while X waits", + file=R3, old="assign x_instr = x_hold_q ? x_hold_instr_q : instr_rdata_i;", + new="assign x_instr = instr_rdata_i;", check=rvf("rabbit3", "liveness_ch0")), +] + + +def make_copy(name): + """Fresh copy of what the formal flows need, under build/mutants/.""" + dst = (WORK / name).resolve() + if WORK.resolve() not in dst.parents: # never delete outside build/mutants + sys.exit(f"refusing to use {dst}") + if dst.exists(): + shutil.rmtree(dst) + def ignore(folder, names): + # build outputs only: build/, __pycache__/, and the SymbiYosys work + # directories next to muldiv.sby (muldiv/, muldiv_/), not the + # testbench files muldiv_tb.sv / muldiv.sby + skip = {"build", "__pycache__"} + if Path(folder).name == "muldiv": + skip |= {n for n in names + if (n == "muldiv" or n.startswith("muldiv_")) and (Path(folder) / n).is_dir()} + return skip + shutil.copytree(REPO / "rtl", dst / "rtl", ignore=ignore) + shutil.copytree(REPO / "dv" / "formal" / "rabbit", dst / "dv" / "formal" / "rabbit", ignore=ignore) + (dst / "third_party").mkdir() + (dst / "third_party" / "riscv-formal").symlink_to(REPO / "third_party" / "riscv-formal") + return dst + + +def run_check(root, check, log): + """True if the check PASSES.""" + with open(log, "w") as f: + rc = subprocess.run(check["cmd"], cwd=root / check["cwd"], stdout=f, stderr=subprocess.STDOUT).returncode + if "status" in check: + st = root / check["status"] + return st.exists() and st.read_text().startswith("PASS") + return rc == 0 + + +def main(): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument("names", nargs="*", help="mutants to run (default: all)") + ap.add_argument("--list", action="store_true") + ap.add_argument("--baseline", action="store_true", help="also check the unmodified copy passes") + args = ap.parse_args() + + if args.list: + for m in MUTANTS: + print(f"{m['name']:24} {m['what']}") + return 0 + todo = [m for m in MUTANTS if not args.names or m["name"] in args.names] + unknown = set(args.names) - {m["name"] for m in MUTANTS} + if unknown: + sys.exit(f"unknown mutant(s): {', '.join(sorted(unknown))} (see --list)") + + WORK.mkdir(parents=True, exist_ok=True) + results = [] + for m in todo: + t0 = time.time() + root = make_copy(m["name"]) + base = None + if args.baseline: + base = run_check(root, m["check"], WORK / f"{m['name']}.baseline.log") + make_copy(m["name"]) # fresh copy for the mutant + src = root / m["file"] + text = src.read_text() + if text.count(m["old"]) != 1: + results.append((m, "NOT APPLIED (RTL changed?)", base, time.time() - t0)) + continue + src.write_text(text.replace(m["old"], m["new"])) + passed = run_check(root, m["check"], root / "mutant.log") + verdict = "caught" if not passed else "MISSED" + results.append((m, verdict, base, time.time() - t0)) + print(f"{m['name']:24} {verdict:8} ({time.time() - t0:5.0f} s) log: {root / 'mutant.log'}", flush=True) + + print("\nmutant result check baseline") + bad = 0 + for m, verdict, base, _ in results: + chk = " ".join(m["check"]["cmd"][-2:]) + b = "-" if base is None else ("pass" if base else "FAIL!") + print(f"{m['name']:24} {verdict:9} {chk:29} {b}") + bad += verdict != "caught" or base is False + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/synth_sky130.sh b/tools/synth_sky130.sh new file mode 100755 index 0000000..2bdd562 --- /dev/null +++ b/tools/synth_sky130.sh @@ -0,0 +1,46 @@ +#!/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 one core +# +# Finds the sky130_fd_sc_hd typical-corner liberty file in $SKY130_LIB, or +# under $PDK_ROOT, or under ~/.ciel / ~/.volare (ciel / volare installs). +# Numbers are a quick comparison, not sign-off: no wires, no placement, and +# ABC's delay varies by about +-0.6 ns between runs of nearly the same RTL. +# Logs: build/synth_sky130/.log +set -euo pipefail +REPO=$(cd "$(dirname "$0")/.." && pwd) +cd "$REPO" + +LIB=${SKY130_LIB:-} +if [ -z "$LIB" ]; then + LIB=$(ls ${PDK_ROOT:-/nonexistent}/sky130A/libs.ref/sky130_fd_sc_hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib \ + ~/.ciel/ciel/sky130/versions/*/sky130A/libs.ref/sky130_fd_sc_hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib \ + ~/.volare/volare/sky130/versions/*/sky130A/libs.ref/sky130_fd_sc_hd/lib/sky130_fd_sc_hd__tt_025C_1v80.lib \ + 2>/dev/null | head -1 || true) +fi +if [ -z "$LIB" ] || [ ! -f "$LIB" ]; then + echo "sky130 liberty not found: set SKY130_LIB=/path/to/sky130_fd_sc_hd__tt_025C_1v80.lib" + echo "(install the PDK with: pip install ciel && ciel enable --pdk sky130 )" + exit 1 +fi + +OUT=build/synth_sky130 +mkdir -p "$OUT" +CORES=${*:-rabbit3 rabbit5 cv32e40p} + +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' ' ') + yosys -p "read_slang $SRC --top rabbit_cpu -DSYNTHESIS; \ + synth -top rabbit_cpu -booth -flatten; \ + dfflibmap -liberty $LIB; \ + abc -liberty $LIB -dont_use *lpflow* -script $REPO/tools/abc_sky130.scr; \ + stat -liberty $LIB" > "$OUT/$c.log" 2>&1 || { echo "$c: synthesis failed, see $OUT/$c.log"; continue; } + area=$(grep 'Chip area for module' "$OUT/$c.log" | tail -1 | awk '{print $NF}') + seq=$(grep 'used for sequential elements' "$OUT/$c.log" | tail -1 | awk '{print $(NF-1)}') + dly=$(grep -oE 'Delay *= *[0-9.]+ ps' "$OUT/$c.log" | tail -1 | grep -oE '[0-9.]+') + printf '%-10s %14.0f %12.0f %12.2f\n' "$c" "$area" "$seq" "$(echo "$dly / 1000" | bc -l)" +done