Module scratchpad_rtl 

scratchpad_rtl — the on-chip scratchpad subsystem in silicon.

The handout claims “SECDED scratchpads” and “double-buffered: compute tile N while DMA streams tile N+1” (CHIP_MEMORY_ANSWERS.md §3, MEMORY_EDGE_SPEC.md). This module makes both real: • a SECDED(72,64) code — single-error-CORRECT, double-error-DETECT — as a Rust oracle (exhaustively tested over every single-bit and a sweep of double-bit faults) and a generated-from-the-same-parity-structure Verilog encoder/decoder, with the single-error-correction property proven by our certified SAT on a tractable Hamming instance and verified bit-exact under iverilog on the full 64; • a double-buffer (ping-pong) controller whose safety invariant — compute never reads the bank the DMA is filling — is checkable by construction.

The SECDED construction is the textbook Hamming-SEC (check bits at power-of-two codeword positions) plus one overall-parity bit for DED. Encoder and decoder are GENERATED from the same position→check-bit incidence, so they cannot diverge.

Enums

Decode

The decode verdict.

Constants

CW_BITS

Total codeword width (72) and data width (64) of the scratchpad ECC.

DATA_BITS

Functions

decode

SECDED decode: a (possibly corrupted) 72-bit codeword → (recovered data, verdict).

emit_double_buffer_verilog

Emit the ping-pong double-buffer controller: swap toggles which bank compute reads (read_bank) vs the DMA fills (fill_bank = ~read_bank). The safety invariant read_bank != fill_bank holds by construction (they are complements).

emit_secded_testbench

Emit a self-checking testbench: encode din, inject a fault pattern from secded_vec.hex (each line: din flip_mask expect_dout expect_corrected expect_double), decode, and compare. Prints PASS/FAIL.

emit_secded_verilog

Emit the SECDED(72,64) encoder + decoder/corrector as synthesizable Verilog, generated from the SAME incidence as encode/decode, so they cannot diverge. Interface: enc takes 64-bit din → 72-bit cw; dec takes a 72-bit cw_in → 64-bit dout + corrected + double_err.

encode

SECDED encode: 64 data bits → a 72-bit codeword (bit 0 = overall parity, bits 1..=71 = Hamming(71,64)).