Binary Circuit Models

Today, evaluating a neural network means interpreting it. The trained weights sit in memory as inert numbers, and a general-purpose machine walks a fetch-decode-execute loop that pushes billions of multiply-accumulates through its arithmetic units to emit each token. That layer of mediation is where inference spends its energy and its latency, and for a model defined over the reals there is no escaping it. A binary model is a different object. Its alphabet is finite, its weights and activations sit at a fixed low precision, and every operation it performs is an exact integer or logical step. Such a model is a total function from finitely many input bits to finitely many output bits, and Shannon's 1937 switching theorem says any such function is Boolean, so it can be laid out as a network of gates -- a circuit.

The paper does not merely note this reduction; it carries it out and measures the result. Earlier work tends to go one of two ways: quantize a model so it runs cheaply on stock hardware, or train a logic-gate network to imitate a task. This work runs in the opposite direction. It takes a finite-alphabet language-model head that has already been trained and compiles it into a circuit computing the identical function bit for bit, then tallies precisely how many gates that takes. The framing shifts from asking how closely logic can imitate a network to asking, given that a binary model is itself a Boolean function, what circuit it corresponds to and what that circuit costs.

Each layer is a multiply-accumulate followed by a nonlinearity. Once binarized, with weights and activations held in one bit as plus-or-minus one, the product of two values is +1 precisely when the two agree, which is precisely when their XNOR is 1. The inner product thus reduces to the familiar XNOR-and-population-count: XNOR gates emit the agreement bits, a balanced adder tree sums them, and a gate-free affine relabel recovers the signed dot product. The threshold nonlinearity is just the high bit of a comparison, and next-token selection is an arg-max tree of comparators. A binarized model, in the end, is built entirely from these three primitives.

A gate-level compiler assembles each block from primitive AND, OR, NOT, XOR and XNOR gates and counts them exactly. The binarized inner product costs 9 to 11 gates per input bit, climbing gently with width as the popcount tree grows deeper: from 146 gates at n=16 to 5,577 gates at n=512, with depth exactly 4*log2(n) levels. One design distinction matters: the block that returns the largest score is not what a language model needs; the head has to emit the index of the winning symbol. Constructed as a balanced tournament tree instead of a linear fold, the 258-way index selector comes to 34,438 gates and is 54x shallower.

Composing the verified blocks at real dimensions yields the size of a model's next-token head directly. For embedding width D=512 over a 258-symbol alphabet, the head is 258 binarized inner products of width 512 plus the 258-way arg-max index tree, totaling 1.47 million gates; at D=768 it is 2.20 million. Mapping with Yosys 0.68 and ABC onto six-input lookup tables, at the measured packing ratios of 3.59 gates per LUT6 for the dot products and 6.20 for the arg-max tree, brings the D=512 head to roughly 0.41 million LUT6, well inside the capacity of a mid-to-large device. On its own, the head of a binary language model is small enough to be a chip.

The full model is another matter. Autoregression is handled cleanly as state: the emitted symbol shifts into a context register and the combinational core re-evaluates on each clock, turning the loop into an ordinary finite-state machine with no instruction stream. But the whole native-binary model at d=128 across four layers costs 24.0 million gates at a 128-key context and 33.5 million at 512 keys. Of the 24.0 million, 13.6 million are the exact-integer datapath and 10.4 million are fixed-point terms that need a multiplier, dominated by 6.0 million gates of LayerNorm. The attention window, not the parameter count, is the lever that determines whether the chip is dominated by mixing or by multiply-accumulates.

The standard of correctness here is bit-exact equivalence, block by block, rather than a benchmark score. Sixteen blocks are proved equivalent to independently written behavioural specifications by SAT over their entire input spaces, not a handful of random draws: 2^128 vectors for the 64-wide inner product, 2^208 for a hard-attention head. The proof harness is validated by a negative control, in which inverting a single output bit flips every case to failed, so a pass is evidence and not just plumbing. All eighteen emitted Verilog modules are additionally co-simulated against the Python netlist under Icarus Verilog, closing the gap that a Verilog printer could be wrong without altering any gate count.

The strongest verification result concerns a real trained layer. Rather than sampling, every one of the 512 neurons of a trained feed-forward layer, with weights baked in, is proved equivalent on its sign bit -- the bit the next layer consumes -- over that neuron's whole 2^128 input space, at a median of 61 seconds each and 1.9 hours of wall time. The full popcount value is proved for 32 of 32 neurons attempted. ABC's combinational equivalence checker, which fraigs both designs before calling SAT, proves an n=128 popcount in 75 seconds where Yosys's monolithic SAT does not finish in forty minutes. Separately, six theorems in Lean 4 formalize the arithmetic identities, including the XNOR-popcount identity and circuit_complete, the Shannon-expansion statement of the thesis, all with no sorry and no added axioms.

A gate count is neither an area nor a watt, so every block is carried through a complete open physical-design flow: Yosys and ABC mapping onto real SKY130 standard cells, then OpenROAD for floorplanning, placement, routing, static timing and power, all in the tt_025C_1v80 corner of the sky130_fd_sc_hd library. Nothing is fabricated; these are what the tools compute from characterized cell tables, so 130nm absolutes serve as a consistent yardstick and the claims are stated as ratios. Switching activity is measured on each netlist rather than assumed, because OpenSTA's uncapped XOR propagation rule drove a popcount's reported power two orders of magnitude above blocks carrying ten times its cell count -- an estimator artifact the paper flags rather than a real cost.

The results restate the cost advantage in placed silicon. The same fan-in-64 inner product built from int8 array multipliers occupies 40.5x the placed area of the binarized version, draws 32.4x the power at matched switching activity, and is 3.0x slower. A gate the compiler emits costs a median 5.0 square micrometres of placed silicon, and the 258-way token selector of a real head is 0.093 square millimetres and 14.55 ns. One compiled neuron of the trained model, pipelined eight deep with clock-tree synthesis, closes at a measured period and emits one result per clock, its pipeline proved equivalent to the combinational version by SAT over the unrolled circuit.

One block stands between this model and an all-integer circuit: LayerNorm. Priced in 16-bit fixed point it needs d squares (hence d multipliers), a reciprocal square root and a per-channel multiply-add. Composed arithmetically from primitive costs, one d=128 LayerNorm comes to 665,373 gates, so the two per block reach 200% of the 664,520-gate matmul they wrap. Building it as an actual netlist from the same primitives gives 844,719 gates, 27% more, because arithmetic composition understates the wiring. The paper replaces it with a multiplier-free shift-normalizer that removes the mean by a wired shift and divides by scale using a leading-one detector and a barrel shifter, recovering the mantissa from a small ROM via conditional adds. When the normalizer's consumer is a sign, the normalization collapses entirely to a per-channel ROM plus one comparator.

Measured as a drop-in swap into a model trained with float LayerNorm, the L2 variant that keeps the exact variance costs +0.0013 bits per token with an interval including zero, for 128 multipliers instead of 384. The fully multiplier-free L1 variant is 266,665 gates, 3.2x smaller than fixed-point LayerNorm with zero general multipliers; it costs +0.398 bits per token but preserves 99.19% of the sign decisions a binarized consumer reads, the penalty coming from normalizers that feed this checkpoint's full-precision attention and head. With shift-normalization and power-of-two output scales, one autoregressive step has no general multiplier anywhere and is 40% smaller.

The device question and the compilation question turn out to be the same question. The trained d=128 checkpoint needs 6.4 million LUT6 and does not fit the largest monolithic FPGA made, exceeding it by 1.6x. But its exact-integer datapath, at 3.48 million LUT6, fits one comfortably, and the redesigned all-integer model maps to 3.7 million LUT6, below the VU19P's 4.1 million budget. The remaining open items, chief among them training a model natively with the shift-normalizer rather than swapping it in, are each a runnable script with a pre-registered success criterion.