Do input-biased random vectors (extreme, sparse, one-hot) catch RTL bugs that uniform random vectors never did?
research/eda-biasdraw
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).
What it found
Extreme-value, sparse, one-hot and mixed input generators, 5,000 vectors each, run against the 26 eda-deepdraw targets (16 proved equivalent, 9 formal timeouts, plus del@122). No generator catches any of them, so none of the 16 equivalence proofs is contradicted, and a bug visible to a given generator among the 9 undecided mutants has per-vector detection probability below 6×10−4 (95%). The del@122 mutant prints 90 output rows for 100 vectors with no wrong value, confirming truncation. Stylised and negative: one design, hand-chosen generators.
Paper, code and results
More in Algorithmic chip-design loops
- 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.
- Can a library-free delay estimate rank accelerator designs by SKY130 critical-path delay better than logic depth?Library-free delay proxies on the generic gate netlist of the 40 MAC engines: gate-type weights leave depth's Spearman 0.611 against SKY130-mapped delay unchanged (0.609), adding fan-out lifts it to 0.83 to 0.90, but gate count alone reaches 0.911, and no proxy recovers the true (area, latency) front.
- How many random vectors does it take to see an RTL bug, and what can 1,280 clean vectors not rule out?Per-vector detection probabilities of the eda-verify mutants: a geometric model fits the random-vector miss rate within 0.005, predicts 45 vectors for a 1% miss, and 1,280 clean vectors cannot rule out a bug rarer than 0.0023 per vector (stylised re-analysis).
- Can RTL checks that need no golden reference model catch the bugs a design loop injects?Five golden-free properties (latency, done pulse, output hold, start-glitch and reset-abort invariance) kill 22 of the 66 killable eda-verify mutants, all control-flow bugs, and none of the 15 ROM or other datapath bugs; the 16 directed vectors catch all 22 too.
- How many SKY130 mappings does a generic-gate screen need to find the best area × latency design?A generic-gate cells × cycles screen puts the best SKY130 area × latency design first among 40 MAC engines; over random pools of 20, mapping 3 designs finds the pool's best 97% of the time, against 15% for random choice.
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.