Do synthesized-netlist features predict which simulation survivors Yosys can prove equivalent?

What it found

Follow-up to eda-equivpredict on the same 27 survivors, now with Yosys installed. Position-free features (cell-count change after synthesis, miter size, identical cell histogram) are scored under leave-one-line-out. None beats guessing the majority class (16 of 27, 59.3%); the source-line rule gets 25 of 27. The nine solver timeouts barely change the netlist (|Δcells| 0 for six), but equivalent mutants span 0 to 178, and miter size is nearly constant (1,188–1,199). A negative result on one design; cone depth and fan-in were not tried (see eda-conehash).

A figure from its own output

Paper, code and results

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

More in Algorithmic chip-design loops

• Do fan-in cone features of a mutant predict which simulation survivors Yosys can prove equivalent?Fan-in cone features (changed sinks, cone gates and depth, registers reached) from hashed gate-level netlists vs which eda-verify survivors are provably equivalent: none beats the 59.3% majority class under leave-one-line-out (best 13 of 27; negative, stylised, one design).
• 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.

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.