Skip to main content

Module crdt_rtl

Module crdt_rtl 

Source
Expand description

crdt_rtl — the CRDT merge unit in silicon.

A CRDT’s convergence is a join-semilattice merge: for a G-Counter the join is the per-replica max (and its value is the sum of the merged lanes). That merge is exactly what logicaffeine_data::crdt::GCounter::merge computes in software. This module emits a fixed-width (4 replicas × 32 bit) hardware merge unit and proves, under iverilog, that its output is byte-identical to that oracle — so a replica’s state converges the same way whether it merged on the CPU runtime or in the chip’s coprocessor.

It is one node’s merge (the commutative/associative/idempotent join). The multi-node distribution protocol (who exchanges state with whom) stays the message-passing layer — honestly a projection, not this block.

Functions§

emit_crdt_merge_testbench
A self-checking testbench: apply N (a,b) vectors and compare merged/value against the oracle from crdt_{a,b,m}.hex (computed in Rust). Prints PASS/FAIL.
emit_crdt_merge_verilog
Emit the combinational G-Counter merge unit: merged[i] = max(a[i], b[i]) across the four 32-bit replica lanes, plus value = sum(merged) (34 bits: 32 + ceil(log2 4)).
emit_dpu_ingest_verilog
Emit the DPU near-data ingest tile: the same per-lane join as crdt_merge, but wrapped in a clocked accumulator — on each posedge clk with in_valid, the state folds the arriving beat into the running join (acc <= merge(acc, in_state)); rst clears it. This is the sequential merge-on-ingest primitive a DPU runs at the data edge: because the join is commutative/associative/idempotent (certified in the_crdt_convergence_order_is_a_total_order_proven_by_our_sat), folding a stream through it is order-invariant — correct even when the controller delivers reads out of logical order. Unlike the combinational crdt_merge unit, this has genuine register-to-register paths, so it is the block that carries meaning through STA/signoff.
merge_lane
The join for one lane — per-replica max, exactly GCounter::merge.