How much does simulation and formal feedback help a proposer repair small Verilog designs?

What it found

A checker (Verilator lint, Icarus lockstep simulation against a golden model, Yosys SAT proof for combinational tasks) scores nine small tasks. With the session itself as proposer, 6 of 9 pass from the spec alone and all 9 after one round of mismatch feedback; the three failures were a Gray encoder written as a decoder, a logical shift on a signed value and a combinational pulse that should be registered. Anecdotal: one attempt per round, one proposer who also wrote the tasks, no resampling baseline, simulation only for sequential tasks. Not an LLM benchmark.

Paper, code and results

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

More in LLM chip design loops

• What does a no-model baseline repair when a scripted RTL checker is the only feedback?No-model mutation-repair baseline for a scripted Verilog checker (compile, lint, simulation, SAT miter) on ten small tasks: 9/20 one-fault cases repaired in 60 evaluations; the session agent passed all ten first try, so the feedback loop is unmeasured. Preliminary.
• Does a rewrite proposer beat a parameter sweep on area and depth when every rewrite must be proved equivalent?Equivalence-gated area/depth rewrites of a 16-bit adder and 6x6 multiplier against a no-model parameter sweep; best adder 0.85x the reference cells×depth, tied by the sweep, no multiplier gain (stylised, gate counts).
• 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.

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.