Khnum — the ram-headed god of memory 𓃝

The Vision

Correct, verified memories — right now, on your laptop.

Most designs don't need a hand-crafted 6T bitcell macro from a seven-figure PDK toolchain. They need correct, verified, portable memories today — SRAMs, register files, FIFOs, ECC — that synthesize to real BRAM on FPGA and harden to real standard-cell layouts through OpenROAD on ASIC, backed by proofs instead of promises.

Honesty is the brand: a checked roadmap box that isn't mechanically true destroys the point of the project. Every claim below is backed by a test, a formal proof, or a routed GDSII layout you can inspect yourself.

The Potter's Wheel

Six memory kinds, one generator.

Every kind ships Verilog-2001 RTL, a self-checking testbench, and a JSON manifest — from one command.

sram_1rw

Single shared read/write port, synchronous read, read-first RDW. The everyday scratchpad.

BRAM-proven ✓

sram_1r1w

Separate write + read ports, same clock. Dual-port scratchpad / cache way.

BRAM-proven ✓

sram_2r1w

One write port, two independent read ports. Register-file-style access.

BRAM-proven ✓

rf_2r1w_ff

Flop-based register file, asynchronous (combinational) reads, depth ≤ 64. The CPU-GPR workhorse.

shipped ✓

fifo_sync

Single-clock FIFO — FWFT, full/empty/level flags, every boundary tested.

shipped ✓

fifo_async

Dual-clock CDC FIFO — Cummings gray-coded pointers, 2-FF synchronizers.

shipped ✓

Plus: transparent --ecc (Hamming SECDED, single-correct/double-detect) on any SRAM kind, and --bank-depth/--bank-width composable tiling into larger arrays.

The Proof

Proofs, not promises — at every level.

✓

Self-checking testbenches

Every generated instance ships a Verilator-driven TB with a shadow-model scoreboard — init sweep, random phase, final sweep.

𓂀

Formal proofs (yosys + z3)

Read-first (incl. per-byte-lane), FIFO occupancy and gray-pointer-validity properties — 9 configs proven, vacuity-checked and mutation-tested.

⚡

A third method: cocotb

Independent Python golden models vs. Verilator sim for all 6 kinds — a verification path distinct from both the Verilog TB and the formal proofs.

⊞

Real FPGA BRAM inference

All 3 SRAM kinds × byte-en on/off genuinely infer RAMB18E1/RAMB36E1 (Xilinx) and SB_RAM40_4K (iCE40) — 12/12 proven via synth_xilinx/synth_ice40, not just asserted.

The Foundry

Real ASIC layouts, on a 16 GB laptop.

DFFRAM-style standard-cell hardening through OpenROAD/ORFS, tuned to stay laptop-safe. Two sizes hardened so far:

design	platform	area (µm²)	util	WNS (ns)	route DRC	peak RAM	status
`khnum_sram_1rw_256x32`	sky130hd	374,736	43%	0.00	0 viol	2.17 GB	✅ timing closed
`khnum_sram_1rw_1024x32`	sky130hd	1,572,503	25%	-0.39	0 viol	8.19 GB	🔧 routes clean, retuning

Full numbers, gotchas, and the exact recipes: harden/HARDEN_RESULTS.md.

The Methodology

A disciplined seven-phase lifecycle.

Every phase ends with a checkpoint commit; nothing advances until tools/test_all.py exits 0. A "partial" is never checked as "done."

P0GenesisPackage + 3 SRAM kinds.

P1Potter's WheelRF, FIFOs, ECC, banking.

P2The ProofFormal + cocotb, vacuity-checked.

P3FPGA GateReal BRAM inference proven.

P4The FoundryOpenROAD/ORFS ASIC hardening.

P5The ScribeDocs, demo, characterization.

P6AscensionPyPI release, v1.0.0.

Why Another Memory Compiler?

A niche neither OpenRAM nor DFFRAM covers.

	Khnum	OpenRAM	DFFRAM
Dependencies	zero (Python stdlib)	Python + packages + PDK setup	Python + packages
Self-checking TB per instance	✅ always, automatically	partial	—
Formal proof per instance	✅ yosys-smtbmc + z3, vacuity + mutation checked	—	—
FPGA + ASIC from one config	✅ portable RTL, BRAM-inference verified	ASIC only	ASIC only
Runs on a 16 GB laptop	✅ hard design constraint	heavy	moderate