What does an all-open RTL flow report for small designs, and can it prove them equivalent?
research/chip-toolchain
Reproducible open RTL flow (Yosys, Icarus, Verilator): gate count and depth for adders, a multiplier and a FIFO, SAT equivalence of two adders plus a broken-adder control. Gate counts, not silicon.
What it found
Installs Yosys, Icarus Verilog and Verilator, records versions, and synthesises adders, a multiplier and a FIFO to a generic gate library: a ripple-carry adder is 5W−3 gates deep 2W−1, and the operator form + gets the same depth with a few more gates. A SAT miter proves the two adders equivalent and rejects a deliberately broken one. Stylised: gate counts, not silicon area; OpenROAD and a PDK are not yet part of the flow.
A figure from its own output
Paper, code and results
More in LLM chip design loops
- Which check catches an RTL bug: lint, random simulation or a formal equivalence proof?What lint, random simulation and a Yosys equivalence proof each catch, on 12 small RTL tasks (companion to
chip-rtl-loop); mutation probe shows 30 of 389 rejected bugs are caught only by the formal proof. Session-written attempts, not an LLM benchmark. - How much does simulation and formal feedback help a proposer repair small Verilog designs?Lint, simulation and formal-equivalence feedback for Verilog repair on nine small tasks; 6/9 pass at round 0 and 9/9 after one round, with the session as proposer (anecdotal, not an LLM benchmark).
- 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 * Ktracks 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).
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.