Module rtl 

RTL / transition-system bounded model checking — including multi-bit (bitvector) registers.

A TransitionSystem is the classic (registers, property) model of synchronous hardware: each Register has a width, an initial value, and a next-state expression over the CURRENT state; a safety property must hold in every reachable state. 1-bit registers are control/FSM bits; wider registers are datapath, handled through the bit-blaster. This module time-indexes the model (r → r@t), lowers it through the certified prover seam (super::sva_to_proof::bounded_to_proof), and drives logicaffeine_proof::bmc. Pure Rust, certified, Z3-free.

parse_transition_system ingests a synthesizable Verilog subset (multi-bit reg, initial, one always @(posedge clk) block, assert property) with a typed (bool / bitvector) expression parser. Unsupported constructs error out — never a silent mis-parse.

Structs

Register

A hardware register: a width, an optional initial value, and its next-state function.

RtlParseError

A Verilog parse error (kept distinct so the BMC layer can surface it verbatim).

TransitionSystem

A synchronous transition system over Boolean and bitvector registers.

Enums

NextState

A next-state function: a direct expression, or a guarded if/else (from RTL reset/mux logic). Guards reference the current state and free inputs.

Functions

emit_alu_datapath_verilog

Emit the GENERAL INTEGER ALU datapath — the combinational functional unit that executes the arithmetic / bitwise / signed-comparison ops straight off a WIRE OPCODE BYTE. The case labels are the stable binisa opcodes (one source of truth with the wire format), so the ALU decodes the same bytes the network carries. Each operation is proven correct by our own certified SAT (the identity battery the_general_alu_datapath_is_proven_correct_by_our_sat); comparisons are SIGNED (matching the VM’s i64 semantics) and yield 0/1. This is the ratchet frontier grown from the reversible core.

emit_isa_core_decoder_verilog

Emit the ISA opcode decoder for the reversible core — the silicon FRONT-END that turns a wire opcode BYTE (the exact byte crate::vm::binisa::encode_program puts on the wire) into the reversible ALU’s 3-bit control select plus a core valid flag. The case labels are DERIVED from crate::vm::binisa::opcode, so the decoder and the wire format share ONE source of truth: the byte the network carries is the byte the chip decodes, with no translation layer. Compose with emit_reversible_alu_core_verilog — wire isa_core_decoder.sel → rev_alu_core.op.

emit_reversible_alu_core_verilog

Emit the LOGOS reversible ALU CORE as synthesizable Verilog — the abelian charge-recovery datapath of the VM: two width-bit registers a,b and a 3-bit opcode selecting RevAdd/RevSub/RevXor/ RevNeg/RevSwap. For every fixed opcode the transition on (a,b) is a BIJECTION, so the whole ALU runs backward with zero erased bits. The 32-bit form place-and-routes on a Lattice ECP5 (ULX3S) via scripts/synth-soft-core.sh (benchmarks/silicon/rev_alu_core.v): 336 LUTs + 64 FFs at ~136 MHz.

emit_reversible_alu_verilog

Emit a synthesizable Verilog SOFT-CORE for the reversible ALU datapath (corner 5, phase 3) — the register-VM’s RevAdd charge-recovery core as RTL: a width-bit register advanced by step each clock. q := (q + step) mod 2^width is a PERMUTATION of the state space (a cyclic reversible datapath whose reverse module is the −step decrement), and the emitted text is real synthesizable Verilog — parse_transition_system accepts it and BMC / k-induction discharge its obligations. This is the round-tripping HDL twin of the software RevAdd; the full VM-datapath soft-core + a VM↔RTL SMT equivalence are the larger MAKE_A_CHIP build this slice opens.

emit_reversible_datapath_verilog

Emit the reversible RevAdd DATAPATH as synthesizable Verilog — a width-bit accumulator advanced by a data INPUT each clock (q := (q + delta) mod 2^width), the genuine charge-recovery ALU slice (its reverse is q := q − delta). For every fixed delta the clocked transition is a bijection in q. Unlike the constant-step emit_reversible_alu_verilog, this is the real datapath the VM’s RevAdd maps to; benchmarks/silicon/ synthesizes + place-and-routes the 32-bit form on an ECP5 FPGA.

emit_shared_divider_testbench

Emit the divider’s self-checking testbench: drive the sequential shared_divider, wait for done, and check quotient+remainder against the combinational $signed div/mod oracle over every sign/edge case plus a 4000-pair pseudo-random sweep. PASS iff all match.

emit_shared_divider_verilog

Emit the SHARED ITERATIVE DIVIDER — one sequential restoring divider that computes signed quotient AND remainder, replacing the ~24,600-cell COMBINATIONAL $signed(a)/$signed(b) + $signed(a)%$signed(b) the ALU instantiates per-op (Div/Mod/FloorDiv). It costs 833 LUT / 204 FF placed-and-routed on the ECP5-85K at ~100 MHz — a ~26× LUT drop vs the ~22,000-LUT combinational divide, the lever that fits the full 113-op CPU under 83,640. Truncated (round-toward-zero) semantics matching the VM: quotient sign = sign(a)^sign(b), remainder sign = sign(a); b==0 → q=r=0. One 1-bit/cycle restoring loop over |a|/|b| (W cycles) then a sign fixup; the soft-core pulses start and stalls until done. The module is Verilog-parameterized (default W=32; instantiate #(.W(64)) for the BigInt lane), so this emitter is the single source for the on-disk shared_divider.v, proven == the combinational oracle by iverilog (emit_shared_divider_testbench).

emit_yosys_tapeout_flow

Emit a yosys synthesis FLOW (.ys) that takes the reversible soft-core RTL to a gate-level netlist (corner 5, phase 5). This is the tape-out-ready boundary produced IN-REPO: the synthesizable, formally-verified reversible RTL (emit_reversible_alu_verilog) PLUS this flow. Executing it needs the external yosys synthesizer (not installed here); mapping the generic gate set to an adiabatic / charge-recovery PDK and running a foundry are the physical tape-out steps beyond software. The flow reads the module, elaborates, techmaps, maps to a generic gate library, and writes the gate-level netlist + a resource report.

lec_next_state_matches_vm

LOGICAL EQUIVALENCE CHECK (corner 5, phase 3) — discharged by OUR OWN certified SAT, not yosys’s SAT or Z3. Parse the soft-core RTL, extract register reg’s next-state, and prove it equals spec (the VM op’s datapath function) for EVERY input by refuting the miter rtl_next ≠ spec with logicaffeine_proof::sat::prove_unsat — a bit-blasted CDCL refutation, the LEC “back-check”. This is the equivalence a tool like yosys equiv runs on its internal SAT, done here on ours. Returns Some(true) iff the RTL datapath is equivalent to the VM spec, Some(false) if a differing input exists, None if the RTL / next-state / miter can’t be lowered to the bit-blaster.

parse_transition_system

Parse a synthesizable Verilog module into a TransitionSystem. Errors (never silently mis-parses) on anything outside the supported subset.