Module handshake_rtl 

Handshake primitives of the spatial IR in silicon: the bounded FIFO (Handshake::Fifo), the counting semaphore (Handshake::Semaphore’s ready counter / valid flag), the arrive-all barrier (Handshake::Barrier) and the one-writer multicast bus (a Group). Each emitter is paired with a trace testbench whose expected values come from the Rust model of the same primitive, and the FIFO’s bound is proven by k-induction with our own certified SAT — the sequential analogue of the combinational proofs the datapaths carry.

emit_fifo_verilog("chan_fifo", 8, 32) is byte-identical to chan_rtl::emit_chan_fifo_verilog(): the language Pipe IS the parameterized FIFO at its recorded parameters (locked).

Functions

emit_barrier_trace_testbench

Staggered arrivals over several rounds: released pulses exactly once per round, on the cycle after the last party arrives, and never otherwise.

emit_barrier_verilog

An arrive-all barrier over n parties: arrivals are sticky; the cycle every party has arrived, released pulses for one cycle and the barrier re-arms.

emit_fifo_trace_testbench

Scripted push/pop trace against a VecDeque model: every cycle the DUT’s pushed, popped, count and (when popped) dout must equal the model’s. Prints PASS: or the first mismatch.

emit_fifo_verilog

A bounded FIFO of depth entries of width bits: FIFO order, full refuses a sender, empty refuses a receiver, dout is the oldest buffered value. Power-of-two depths wrap their pointers naturally; other depths compare explicitly.

emit_mcast_bus_trace_testbench

Sends, idles and back-to-back sends: every receiver’s push and dout follow the writer one cycle later.

emit_mcast_bus_verilog

A one-writer multicast bus: on send, the next cycle every one of the n receivers sees push with the same dout — the multicast landing of a Group (each receiver pushes it into its own FIFO).

emit_semaphore_trace_testbench

Scripted set/inc/threshold trace against the Rust model of the semaphore.

emit_semaphore_verilog

A counting semaphore of width bits: set loads set_val (the owner’s reset), else inc adds inc_n (a remote increment); ge is count >= thresh — the set / increment / wait-threshold discipline every dataflow mesh’s semaphores implement.

fifo_bound_certified

0 ≤ cnt ≤ depth for EVERY push/pop stream, by k-induction over the FIFO’s count register exactly as the RTL computes it (popped = pop ∧ cnt≠0, pushed = push ∧ cnt≠depth).