Does a rewrite proposer beat a parameter sweep on area and depth when every rewrite must be proved equivalent?

What it found

A loop in which rewrites of a 16-bit adder and a 6×6 multiplier must be proved equivalent to the reference by a Yosys miter before a generic-gate ABC script scores cells and depth. With nine attempts written by the session agent (not an LLM benchmark; two were seeded faults the gate rejected), the best adder is a 4-bit carry-select at 0.85× the reference cells×depth, the same circuit family as the best config of a no-model parameter sweep, so a random sweep of the same budget never beats it (ties in 63 of 200 seeds). No multiplier rewrite beat a * b. Stylised: gate counts, not layout; one tool version; two designs.

A figure from its own output

Paper, code and results

• README and method
• Experiments and results
• Code
• Tests

More in LLM chip design loops

• How does generic-gate area grow with bit width for adders, shifters, popcount and multipliers?How generic-gate cells and depth scale with bit width for seven arithmetic blocks: adder, comparator and mux are near-linear, the multiplier quadratic (exponent 2.19), and adder depth grows ~2×W (stylised, generic gates).
• Does writing a fixed-weight multiplier as shift-and-add with canonical signed digits beat Yosys's x * K?Fixed-weight multipliers for all 255 8-bit constants: Yosys's x * K tracks binary shift-add (Pearson 0.97 with set bits), and a canonical-signed-digit form has 33% fewer generic-gate cells at similar depth (every form proved equivalent).
• Does sharing sub-sums across a bank of fixed-weight multipliers cut gates beyond per-constant shift-and-add?A bank of fixed-weight multipliers sharing sub-sums (multiple-constant multiplication): 9% fewer generic-gate cells than per-constant signed-digit shift-add at 2 constants and about 20% fewer at 8 and 16 (43% fewer than Yosys's *), every form proved equivalent; random constants, not trained weights.
• How many gates could an exact 4-input rewriter still remove from Yosys/ABC netlists?How many gates an exact 4-input rewriter could still remove from real Yosys/ABC netlists: none in 28 of 30 runs (1 gate in two), even where the default script beats plain mapping by 25 to 42%, so the flow's gains are not local.
• How many gates above the proven minimum does Yosys/ABC use for 4-input logic?How far above the SAT-proven minimum gate count Yosys/ABC lands on 4-input logic: the default flow is exactly optimal on only 34% of sampled functions (mean 1.19 gates above, max 4), and a heavier script is worse.
• Does the ABC synthesis script matter as much as the written RTL structure for adder and multiplier area and depth?Sweeps five ABC scripts over five adder and eight multiplier structures (all proved equivalent): the script moves cells×depth by up to 1.75× for one adder, while all eight multiplier structures score identically (stylised, generic-gate).

All 40 LLM chip design loops projects →

Other research topics

Proper scoring & elicitation28Effort & peer prediction9Verification games & slashing19Detection & tolerances14Markets as routers13Prediction-market design9Paying contributors8Decentralised training systems23Digital twins & sim-to-real164LLM chip design loops40Robot manufacturing loops53Ambient AI assistant46Self-replicating manufacturing34Simulation-first design64Engineered clothing45Task-specific AI accelerators40Algorithmic chip-design loops42Open-source purpose-built robots44The software-engineering loop43Adversarial human imitation41Open-source residential construction41Autonomous multi-angle capture34Sensing, imaging and 3D31Energy supply and dense energy storage39Robot societies among people31Agentic co-design of low-cost robots27Laundry-hanging robots25Machine learning on qualitative data23Robots on the building site27Civilizations & group psychology1History & human sciences1

Produced with AI assistance (Claude). Results are from the code in this repository and are simulated or stylised unless the abstract says otherwise; nothing here implies affiliation with or endorsement by any lab, researcher or company cited. MIT licensed.