Expand description
infinichip_rtl — the integrated Infinichip memory subsystem, taken all the way to a signoff-clean Sky130 GDSII.
Stage 1 tapes out the command player alone (codegen_sva::dram::dram_executor). Stage 2 —
here — composes the product: one infinichip top-level that wires three INDEPENDENTLY
CERTIFIED sub-blocks into a single manufacturable die:
• the command player — the deterministic DRAM command-stream executor (dram_executor);
its plan-word decode and countdown issue-timing are proven by our OWN SAT in
codegen_sva::dram;
• the SECDED(72,64) ECC on the data path (secded_enc/secded_dec, codegen_sva:: scratchpad_rtl) — single-error-correct, double-error-detect, exhaustively verified and
Hamming-SAT-proven;
• the double-buffer (double_buffer) — ping-pong bank select whose safety invariant
read_bank != fill_bank holds by construction.
Because each sub-block carries its own proof, the integration’s remaining obligation is that
the WIRING composes correctly — discharged by the self-checking tb_infinichip iverilog
testbench (command stream issues, ECC corrects a single fault, banks stay disjoint), and the
data-integrity of the composed ECC path is re-checked here against the certified SECDED oracle.
The emitted infinichip.v is SELF-CONTAINED (every sub-module definition is inlined), so the
OpenLane/Sky130 flow tapes it out from a single PDK-agnostic source, exactly like the other
blocks: scripts/openlane-run.sh infinichip clk <period_ns> infinichip.v.
Functions§
- emit_
infinichip_ testbench - Emit a SELF-CHECKING integration testbench: it drives all three datapaths through the composed
infinichiptop and asserts (1) the ECC read path corrects a single-bit fault and recovers the data one edge after the codeword arrives, (2) the double-buffer banks stay disjoint across a swap, and (3) the command player issues a loaded command with the exact decoded payload. Prints PASS/FAIL — no external vectors needed. - emit_
infinichip_ verilog - Emit the SELF-CONTAINED
infinichip.v: every certified sub-block definition inlined, followed by the structural top. One PDK-agnostic file → tapes out on Sky130 with no cross-file deps.