Can an SMT bounded model check (z3) settle the 10 RTL mutants that Yosys' SAT and induction left undecided?
research/eda-smtbmc
Z3 bounded model checking via yosys-smtbmc decides none of the 10 undecided eda-deepdraw survivors at the 24-cycle depth a full inference needs; its cost passes from about 3 s at depth 10 to over 240 s at depth 12.
What it found
The 10 survivors that Yosys' SAT and induction left undecided (including the known-truncating del@122) were re-checked with yosys-smtbmc and z3. At depth 24 (one inference is 20 cycles) all 10 time out at 900 s; a depth sweep on two targets passes to depth 10 in about 3 s and times out at depth 12 (240 s limit), so the route is no stronger than the built-in SAT at the depth that matters. A pass at depth 10 is not an equivalence claim: the sweep includes a mutant that simulation shows is killable. Negative result: one design, one solver (Yices and Boolector were not installable here), word-level encodings not tried.
Paper, code and results
More in Algorithmic chip-design loops
- Does the systolic-array versus MAC-lane verdict survive a shared SKY130 clock target?The 24 systolic-array and MAC-lane designs of chip-systolic mapped to SKY130 at six shared clocks: the MAC-lane engine keeps the best area x latency at every feasible target (arrays 1.61 to 1.66x worse), though the clock removes many arrays and changes the Pareto front.
- What does a good die cost, and at what area do chiplets beat one big die?Cost per good die from five yield models, a dies-per-wafer count and sourced wafer prices and defect densities: a 600 mm² die costs about $179 on a 7nm-class and $359 on a 5nm-class wafer, the yield model moves the 5nm figure by 16%, and two chiplets beat one die from about 300 mm² of logic (range 126-728 mm² over packaging cost and defect density).
- How much of an open-source chip design search can cheap fidelity rungs and proof prediction save, with a guarantee?Milestones 1 to 3 done: on 10 designs x 60 ABC pass sequences, the generic-gate score does not rank like routed SKY130 area x delay (tau-b median -0.04), and liberty mapping mis-ranks too when the clock is tight (tau 0.59); at equal wall-clock a one-shot cheap-rung screen does not beat random or hill-climbing search on the cached table; successive halving across rungs does not beat random routed search on mean regret either (plain halving from the generic-gate rung is worst; a 6-point routed pilot to pick the start rung fixes most of that, H3), a 10-point routed pilot plus a conformal bound on the mapped rung keeps the routed optimum 0.99 of the time (nominal 0.90) at 42 to 57% of the routed runs, but on the generic-gate rung coverage fails (0.65 against 0.80, H4 refuted there); proof-success prediction (H5): pooled AUC 0.96 to 0.998 across 15 designs is just design size (an oracle knowing only each design's success rate scores the same), and inside the one design with variation it is 0.65 to 0.78, so H5 is not supported; milestone 6 proves that halving's routed regret is at most the sum of the cut rungs' largest ranking inversions (vacuous for the generic-gate rung, loose for the mapped ones); milestone 7a adds a distribution-free pilot quantile of pair inversions (16-point pilots hold the nominal 0.8 coverage in all 60 group-rung cells, median 0.32 of the maximum), whose summed bound is under 0.1 on 9 of 10 groups for the mapped rungs at a relaxed clock but is violated by realised halving regret in 1 of 40 cells, so it is a heuristic, not a guarantee
- Can one harness check, score, cache and log candidate chip designs for any proposer?Unattended design loop (lint, bit-exact RTL sim, gate-netlist check, Yosys synthesis, hash cache, JSONL log, pluggable proposers) run on
chip-accel's 40-design grid: synthesis and the gate check are 99% of wall time (stylised, generic-gate counts, no place and route). - Does a space-filling grid order beat the harness's lexicographic order on other chip-design families, or was that luck of one table?Does a space-filling grid order beat the harness's lexicographic one on other families? Lexicographic is arbitrary (worst on MAC, best on FIR); farthest-point beat random from about 6 evaluations on every table, and
eda-harnessnow offers it as an option (stylised, two 36-design families). - Does the order a grid proposer walks a chip-design space change how quickly it finds the Pareto front?Does the order a grid walks a design space matter? The harness's lexicographic grid trails every random order to 30 evaluations; Halton reaches 90% of the front in 7 evaluations against 17 for random (stylised, one table, deterministic orders are single draws).
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.