Do fan-in cone features of a mutant predict which simulation survivors Yosys can prove equivalent?

What it found

The next step eda-conefeat named. Golden and mutant are lowered to gate level without ABC, and each flip-flop and output is compared by a Merkle hash of its fan-in cone. Features of the changed cones (count, gates, depth, leaves, registers reached downstream) are scored under leave-one-line-out on the same 27 survivors. None beats the 59.3% majority class (best 13 of 27). One observation, found after looking at the table: all seven survivors that change exactly one sink are literal edits on two lines, and none is provably equivalent (six of the nine solver timeouts are among them). One design, one solver, stylised.

A figure from its own output

Paper, code and results

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

More in Algorithmic chip-design loops

• Is the farthest-point spread's lead over random draws, when adapting a chip-design cost model to a new family, bigger than split noise?eda-adaptfixed re-run with 40 splits per family and bootstrap intervals: for the linear model the spread beats random draws at every k (about 1 point of error at 3 to 8 designs, 2.5 at 2), but for ridge it loses at 3 designs and one family (sorter) reverses the sign, so the pooled interval is narrower than the real uncertainty.
• Does the farthest-point spread's lead over random draws, when adapting a chip-design cost model to a new family, survive resampling the designs themselves?eda-adaptci re-run with a design-level bootstrap: the intervals widen by up to 2.5x, the spread's lead holds at 5 and 8 designs for both models (about 0.5 to 1.1 points) and at 2 for the linear model, but the linear k = 3 lead and the ridge k = 2 lead include zero, and the ridge k = 3 loss reported earlier is not established.
• How many placed designs from a new family does an area surrogate need, and does the answer change when the target is placed area instead of a synthesis cell count?The eda-adapt few-shot curves refitted to OpenROAD-placed area on 133 SKY130 designs: an unseen family's placed area is off by 39% (ridge), one placed design cuts it to 23%, about three reach 20%, as for cell counts.
• Do input-biased random vectors (extreme, sparse, one-hot) catch RTL bugs that uniform random vectors never did?Four biased generators (20,000 vectors per target) catch none of the 26 eda-deepdraw survivors, so none contradicts a formal equivalence proof, and the del@122 mutant is confirmed as truncated output (90 rows for 100 vectors).
• Do the SKY130 area and latency conclusions for a MAC-engine family survive a target clock period?The 40 MAC-engine designs mapped to SKY130 at six shared clock targets: cell count still ranks area (Spearman 0.995+), logic depth ranks delay at only 0.34 to 0.82, and with one shared clock the Pareto front equals the generic one, so the earlier front change came from per-design clocks.
• Do 20,000 random vectors catch any RTL bug that 64 missed, and do they contradict the formal equivalence proofs?20,000 further random vectors catch none of the 25 eda-verify survivors, so none contradicts a formal equivalence proof; a random-visible bug among the 9 formal timeouts has per-vector detection probability below 1.4e-4.

All 42 Algorithmic 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.