Pith. sign in

REVIEW 4 major objections 7 minor 41 references

Rethinking Logic Optimization Operators: Theory-Derived Operator Compression via Agentic Source Analysis

T0 review · 4 major / 7 minor · reviewed 2026-07-30 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Pinned logic-synthesis operators admit certified source-level relations that shrink the action menu and skip provably idle evaluations without changing outputs.

desk verdict Solid implementation-scoped operator theory for EDA: the 40→31 cover and bit-identical gates are real contributions, with risk concentrated in two audit-only source premises rather than in the experiments. read the letter →

arxiv 2607.23672 v1 pith:GTOH4FRT submitted 2026-07-26 cs.LO

Keren Zhu This is my paper · ORCID
classification cs.LO
keywords logicsynthesisoperatorcompressionadmissiongatesAIGorchestrationParetocoveragenticsourceanalysismultileveloptimizationABC
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Modern logic synthesis treats many rewrite, resubstitution, refactoring, and carrier-script operators as opaque choices in a huge search space. This paper argues that much of that menu is redundant once you read the actual pinned implementations: some stages discard their results, some variants are nested inside larger ones, and some evaluations are idle on identifiable local structure. Using agent-assisted readings of fixed ABC and mockturtle source, adversarially audited and registered as claims, it derives a two-layer compression: unconditional aliases and dominance collapse forty recipe actions to a thirty-one-action exact one-recipe Pareto cover, and state-conditional predicates become deterministic admission gates. Plugged into ABC Orchestrate as TACO, two exact gates cut runtime by eleven percent with bit-identical outputs on sixty-six circuits, and the gated system uses fewer nodes on fourteen of sixteen reported circuits while running several times faster. A sympathetic reader cares because the bottleneck shifts from ever-larger sequence search to a smaller, justified vocabulary with skips that preserve trajectories.

What carries the argument

The two-layer compression hypothesis, realized by agentic source analysis: universal fixed-scope quotients (identities, aliases, nested variants, metric dominance) plus sound structural admission predicates (sterile, dedupe, accounting gates) that compile into a registry-backed gate layer inside the published orchestration backbone.

What would settle it

Exhibit one legal input where a registered exact identity or sterile gate changes the network or trajectory, or where the thirty-one retained recipe actions fail to match the original forty-action one-recipe node-depth Pareto frontier on some legal recipe input.

Watch

Extended reading notes

Core claim

From pinned ABC and mockturtle semantics, certified operator relations yield theory-derived compression: forty deployed recipe actions collapse to a thirty-one-action exact one-recipe Pareto cover, and source-level conditions compile into deterministic admission gates. Integrated as TACO, those gates accelerate and improve orchestration under fixed backbones, with two exact gates alone giving eleven percent less runtime and identical outputs on all sixty-six tested circuits.

Load-bearing premise

The load-bearing premise is that adversarially audited, human-adjudicated readings of pinned source correctly prove each claimed identity or skip at its stated scope, without machine-checked proofs of those obligations.

Editorial extensions

If this is right

  • Sequence- and policy-search methods can start from a thirty-one-action certified recipe basis instead of the full forty-action menu without losing one-recipe Pareto endpoints.
  • Exact sterile and dedupe gates can be dropped into other orchestration paths as trajectory-preserving plugins, as TACO-skip does for stock Orchestrate.
  • Per-root and per-pass idle regions become compile-time admission checks rather than runtime trials, cutting wasted engine evaluations.
  • Cross-carrier complementarity and polarity-erased fiber obstructions mark which remaining choices must stay dynamic and which structural languages cannot fully certify them.
  • A replayable claim registry of scoped relations becomes a reusable interface between implementation semantics and optimizer design.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same weakest-first measure–draft–audit loop could compress operator menus in other mature EDA or compiler pass stacks where guards and discarded returns accumulate silently.
  • If mixed-fiber witnesses were found for the still-open function-dependent engines, larger fractions of residual evaluation could move behind structural or cheap function-aware gates.
  • Machine-checked proofs of the finite registry obligations would turn the current audit trail into a stronger trust base without changing the executable gate layer.
  • Learned orchestrators trained on the compressed basis may spend capacity on true order sensitivity instead of rediscovering aliases and dead stages.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 7 minor

Summary. The paper proposes "agentic source analysis": LLM agents draft operator-level relations from pinned ABC (bcfdf59) and mockturtle (fb8f879) source trees, independent adversarial audits test them, and surviving claims enter a replayable registry. Three families of results follow. (i) A fixed-scope quotient: 40 deployed recipe actions (H00–H39, inherited from LSOracle/HeLO) collapse to a 31-action exact one-recipe Pareto cover (Corollary 5), via a discarded-return lemma (Lemma 4), an inert-saturation-flag argument (U-SAT), and one metric dominance; two tempting further merges are refuted by exhibited witnesses. (ii) Sound admission predicates: sterile/dedupe/accounting gates (Theorems 12–15) with self-contained combinatorial proofs, plus an XMG–MIG collision necessity theorem (16) and a polarity-erased fiber obstruction (18) with an exhibited cut-4 witness. (iii) A system: TACO inserts the gate layer into ABC Orchestrate; TACO-skip gives bit-identical outputs on all 66 circuits with 11% runtime reduction; integrated TACO improves nodes on 14/16 Orchestrate circuits (geomean 0.990 nodes, 0.968 levels) at 2.6× speed; TACO-max reaches 0.903 NDP geomean on HeLO's three exact-input rows. Claims are carefully scoped (one-recipe frontiers only; measurements quantified over named corpora; Tier-2 gates carry registered residuals).

Significance. If the results hold, the paper contributes a genuinely useful methodology and a set of reusable proof objects: source-derived sterile/dedupe gates that plug into a production flow with bit-identical outputs and an 11% same-algorithm speedup, plus a disciplined framework (quotients, predicates, witnessed obstructions) for reasoning about operator vocabularies in mature synthesis tools. The strengths are concrete and checkable: pinned commits (ABC bcfdf59, mockturtle fb8f879), 66/66 byte-level bit-identity, a final 552/552 CEC sweep, two independent NPN decoders (222/222 classes), exhibited counterexample witnesses for the non-collapsible pairs and the fiber obstruction, and a released artifact with a claim registry and preserved refutation trail. The QoR gains of integrated TACO are modest but honestly measured on a held-fixed backbone. The main limitation is that the most consequential theory result — the 40→31 exact cover — is certified by adversarial audit rather than mechanically, a gap the authors themselves acknowledge (§VIII-E) but which, at a logic venue, deserves at least the cheap de-risking steps outlined in the major comments.

major comments (4)
  1. [§II-B, Lemma 4 / Corollary 5 / Appendix A–B] The headline result rests on two audit-only premises. Eight of the nine removals (seven via Lemma 4 case (i): H11, H18, H21–H23, H28, H33; one via U-SAT: H19) depend on source readings that are not machine-checked and are checked empirically only by corpus enumeration, while Corollary 5 quantifies over 'every legal input.' The paper's own Appendix U documents this exact failure mode (a harness that discarded a returned network). Proportionate fix: (i) reproduce in the paper the line-level anchors for Properties 1–2 and the record-counter claim; (ii) add randomized differential testing of each alias class (H04 vs H11/H18/H19; H06 vs H21–H23/H28; H09 vs H33) on generated inputs beyond the corpus; (iii) instrument the FR saturation loop's record count to log zero refires. All three are cheap and within scope.
  2. [Appendix A, proof of Lemma 4] As stated, Lemma 4 covers 'any recipe stage that invokes cut rewriting without binding the returned network,' but Appendix A's induction silently assumes all other recipe stages interact with the persistent network only as pure readers or in-place operators, and that κ is side-effect free (Property 1) — a global property of the recipe framework, asserted rather than exhibited. Property 1 (immutable reference, outcome as returned value) also appears in tension with mockturtle's typical in-place algorithm signatures; the paper should exhibit the exact pinned signature of the called operator and enumerate the actual WØ call sites in the LSOracle/HeLO scripts, making the unbound-return premise checkable by a reader directly rather than only via the released registry.
  3. [§VII-C / Table XII vs. Table XIX–XXIII] The primary 0.903 NDP claim compares TACO-max (iterative 20-pass AIG pre-pass, 60 MIG rounds, doubled time) against HeLO's published values at presumably fixed effort; aes_core runs 1941 s vs HeLO's reported 63 s (cross-machine caveat noted). What is missing is an attribution ablation: TACO at normal (non-max) effort on the three exact-input rows is never reported (only TACO-fast is, at 0.940). Without it, the reader cannot separate the contribution of the certified gate layer from that of the enlarged effort budget. Please add the normal-effort TACO row on exact inputs and state in the abstract that the 0.903 figure is at maximum effort.
  4. [§VI / Table VI] Agentic source analysis is advanced as a paradigm and is the trust backbone of every U-*/G-* claim, yet §VI is qualitative: no count of registry entries by status, refutation rate, models used, or audit-outcome statistics. Appendix X lists six refutations, which is valuable, but a summary table of the full campaign (drafts submitted, withdrawn, refuted, narrowed; which audits caught what) is needed for a reader to calibrate the acceptance-by-adjudication step, especially given the failure modes in Table XXIV.
minor comments (7)
  1. [Abstract; Table XI] Typesetting: missing spaces throughout the abstract ('formTACO', 'TACOuses', '2.6×faster', '0.903on'); Table XI case names contain stray spaces ('b17 1', 'b18 1').
  2. [Fig. 1] Fig. 1(a) uses 'xag_script' and 'WØ' before either is defined (WØ is only explained in Table XIII); define at first use or in the caption.
  3. [§VII-A1, Table VIII] Each gate alone recovers 4.1 s of the combined 4.2 s, so the two firing regions nearly coincide; a sentence quantifying the overlap of skip sites (and noting that one gate may suffice in practice) would sharpen the attribution.
  4. [§II-A, Definition 2] It would strengthen the motivation to state explicitly that HeLO's usage — one fixed script per subcircuit — makes the one-recipe frontier of Definition 2 the operationally relevant scope, so the quotient's limitation relative to multi-step flows does not restrict its intended application.
  5. [§III-A, Theorem 15] Part (ii) ('|MFFC(n)| ≥ 8 and a genuine cut admits an offer') uses u(c) ≤ s*; Appendix I notes structural-hash reuse can lower u(c) below s*, making the bound conservative — a one-line cross-reference in the theorem statement would prevent misreading. Also verify the stored-size histogram is reproducible from the released decoder (222/222 is claimed in Table XXV).
  6. [§II-A, Table II] The term R(D, A) is defined but used essentially once; 'stored sizes ∗' in Table II is awkwardly typeset; consider trimming.
  7. [§VII-B / Table XI] The sqrt +1.2% node regression is conjectured to come from zero-gain moves declined by the new commit rule; since Lemma 7(a) already characterizes the strict/zero-gain relationship, a one-root diagnostic confirming this on sqrt would close the loop.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: operator relations are discharged against pinned external source trees; experimental baselines and bit-identity checks are independent of the compression narrative.

full rationale

The load-bearing derivation (Lemma 4 → alias classes → Corollary 5 / U-Q31; Theorems 12–16 for gates) reads pinned ABC/mockturtle implementations and proves scoped identities, aliases, containment, and sterile/dedupe predicates. Those premises are external code semantics, not quantities fitted from the paper’s QoR tables. Definition 2’s one-recipe Pareto cover is an explicit, limited mathematical target (frontier equality under one-action endpoints), not a self-definition of the retained menu; multi-step reachability and minimum cardinality are openly excluded. Experimental claims are measurements against published Orchestrate and HeLO numbers, plus 66/66 bit-identity and CEC checks—none of which re-enter the source lemmas as inputs. Author adjudication of adversarial audits and the optional TACO-fast in-sample tuning are verification/effort-scope issues, not circular reductions of a claimed first-principles prediction to its own fit. Self-citation of the author’s unrelated LLM routing note is methodological precedent only and is not used to force the 40→31 cover or the gates. No step reduces a central prediction to a fitted parameter or a load-bearing self-citation chain.

Assumptions & free parameters 3 free parameters · 6 assumptions · 3 invented entities

The central compression claim rests on taking pinned implementation semantics as ground truth, on scoped endpoint equality (not multi-step search equivalence), and on a human+LLM audit process rather than formal proof assistants. Experimental claims further depend on benchmark manifests and protocol choices for effort. No physical constants; free knobs appear mainly in optional fast/max schedules, not in the exact-gate core.

free parameters (3)
  • TACO-max AIG pre-pass / MIG-round / time caps = ≤20 AIG iters; ≤60 MIG rounds; T=1800s class limits
    Iterative fixpoint ≤20 AIG passes, ≤60 MIG rounds, doubled time budget chosen to align effort with HeLO; affects NDP comparison, not the 31-cover theorem.
  • TACO-fast empirical overlay bounds = RF 9/14; RW keep 100; gain stop 0.5%; windows 4096/3
    RF 9/14, RW keep 100, gain<0.5% stop, yield windows 4096 / 3 rounds selected on development corpus; optional and separated from main TACO.
  • Tier-2 residual acceptance (e.g. G-P6)
    Boundary gates retained with measured residuals (s38417 NDP 136918 vs 137173) rather than trajectory certificates; threshold of acceptable residual is author judgment.
assumptions (6)
  • domain assumption Pinned ABC/mockturtle/LSOracle commits define the operator semantics under study; theorems quantify over Simpl of those trees.
    §II-A; all certificates are implementation-scoped, not representation-abstract.
  • ad hoc to paper Exact Pareto cover means equality of one-recipe node-depth frontiers only (Definition 2); multi-step trajectories and minimum cardinality are out of scope.
    Explicitly limits Corollary 5; readers might over-read ‘compression’ as full flow equivalence.
  • ad hoc to paper Structural predicates may use only polarity-erased typed multigraph structure (Definition 10); function data is outside sterile completeness.
    Underpins Theorem 18 mixed-fiber obstruction and the dynamic residue boundary.
  • domain assumption Discarded pure cut-rewrite returns leave persistent state unchanged (Lemma 4 purity + value guard).
    Local source premise for the largest alias collapse in the 40→31 cover.
  • ad hoc to paper Registry acceptance after independent adversarial audit plus author adjudication is sufficient to mark claims CURRENT.
    §VI; substitutes for machine-checked proof in the trust chain.
  • standard math Standard Boolean network / AIG-MIG-XAG-XMG multilevel synthesis model and NPN cut rewriting accounting.
    Background from Brayton/MIS/SIS, Mishchenko DAG-aware rewriting, Amarú MIG, etc.
invented entities (3)
  • Two-layer compression hypothesis (fixed-scope quotients + sound admission predicates + mixed-fiber residue) independent evidence
    purpose: Organize which operator relations can be certified vs must stay dynamic.
    Core conceptual frame in §II; not a physical entity but a new analytical decomposition.
  • Agentic source analysis loop with claim registry independent evidence
    purpose: Make lemma-scale reading of production optimizers tractable and auditable.
    Method contribution; falsifiable via released audits/refutations (Appendices U–X).
  • TACO / TACO-max / TACO-skip gate-conditioned optimizer family independent evidence
    purpose: Executable realization of certified gates inside ABC Orchestrate and HeLO-style protocol.
    Engineering artifact; evidence is QoR/runtime/CEC measurements.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Rethinking Logic Optimization Operators: Theory-Derived Operator Compression via Agentic Source Analysis." pith.science (2026). https://pith.science/paper/GTOH4FRT

@misc{pith2026260723672,
  author       = {Pith},
  title        = {Pith review of: Rethinking Logic Optimization Operators: Theory-Derived Operator Compression via Agentic Source Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GTOH4FRT}},
  note         = {Machine review of arXiv:2607.23672}
}
read the original abstract

Logic synthesis has evolved from compact two-level minimization to large multilevel flows with many interacting optimization operators. Recent work has invested substantial effort in sequencing these operators: actions are commonly treated as opaque choices in a rapidly expanding search space, while learned circuit representations and heuristic or local-greedy orchestration provide increasingly informed ways to explore it. A central obstacle is the operator vocabulary itself. Production operators are numerous, span different representations and mathematical foundations, and expose behaviors determined by implementation-level guards, bounds, and update order. We address this gap through agentic source analysis, using LLM agents to formulate operator-level relations from pinned ABC and mockturtle implementations and adversarial audits to test their stated scope. The resulting certified relations yield theory-derived operator compression: 40 deployed recipe actions collapse to a 31-action exact Pareto cover, and source-level conditions compile into deterministic admission gates. We integrate these gates directly into ABC Orchestrate to form TACO. Two exact gates reduce Orchestrate runtime by 11% with bit-identical outputs on 66 circuits. In a held-fixed integrated comparison, TACO uses fewer nodes on 14 of 16 circuits, with geometric-mean reductions of 1.0% in nodes and 3.2% in levels, while running 2.6x faster. TACO-max achieves an NDP geometric-mean ratio of 0.903 on HeLO's three exact-input rows.

Figures

Figures reproduced from arXiv: 2607.23672 by the authors.

Figure 1
Figure 1. A concrete quotient and the layered system. (a) In [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. The divergence trigger. (a) The self-referential shape: [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. The smallest MAJ-compressible gap: MAJ3 requires four AIG ANDs [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The agentic source analysis loop. Usage is measured in the deployed [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 3 linked inside Pith

  1. [1]

    R. K. Brayton, G. D. Hachtel, C. T. McMullen, and A. Sangiovanni- Vincentelli,Logic Minimization Algorithms for VLSI Synthesis. Kluwer, 1984

    1984

  2. [2]

    Mis: A multiple-level logic optimization system,

    R. K. Brayton, R. Rudell, A. Sangiovanni-Vincentelli, and A. Wang, “Mis: A multiple-level logic optimization system,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1987

    1987

  3. [3]

    Sis: A system for sequential circuit synthesis,

    E. M. Sentovich, K. J. Singh, C. Moon, H. Savoj, R. K. Brayton, and A. Sangiovanni-Vincentelli, “Sis: A system for sequential circuit synthesis,” UC Berkeley, Tech. Rep., 1992

    1992

  4. [4]

    Dag-aware aig rewriting: A fresh look at combinational logic synthesis,

    A. Mishchenko, S. Chatterjee, and R. Brayton, “Dag-aware aig rewriting: A fresh look at combinational logic synthesis,” inProc. DAC, 2006

    2006

  5. [5]

    Scalable don’t- care-based logic optimization and resynthesis,

    A. Mishchenko, R. Brayton, J.-H. R. Jiang, and S. Jang, “Scalable don’t- care-based logic optimization and resynthesis,”ACM Transactions on Reconfigurable Technology and Systems, 2011

    2011

  6. [6]

    Sat- based exact synthesis: Encodings, topology families, and parallelism,

    W. Haaswijk, A. Mishchenko, M. Soeken, and G. De Micheli, “Sat- based exact synthesis: Encodings, topology families, and parallelism,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020

    2020

  7. [7]

    Boolean rewriting strikes back: Reconvergence-driven windowing meets resyn- thesis,

    H. Riener, S.-Y . Lee, A. Mishchenko, and G. De Micheli, “Boolean rewriting strikes back: Reconvergence-driven windowing meets resyn- thesis,” inProc. ASP-DAC, 2022

    2022

  8. [8]

    A simulation-guided paradigm for logic synthesis and verification,

    S.-Y . Lee, H. Riener, A. Mishchenko, R. Brayton, and G. De Micheli, “A simulation-guided paradigm for logic synthesis and verification,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022

    2022

Show all 41 references
  1. [9]

    Majority-inverter graph: A new paradigm for logic optimization,

    L. Amar `u, P.-E. Gaillardon, and G. De Micheli, “Majority-inverter graph: A new paradigm for logic optimization,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2016

    2016

  2. [10]

    Logic optimization with xor-and graphs,

    E. Testa, M. Soeken, A. Zulehner, L. Amar `u, and G. De Micheli, “Logic optimization with xor-and graphs,”IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems, 2020

    2020

  3. [11]

    Logic optimization with majority-inverter graphs and xor-majority graphs,

    M. Soeken, E. Testa, A. Mishchenko, and G. De Micheli, “Logic optimization with majority-inverter graphs and xor-majority graphs,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2019. 12

    2019

  4. [12]

    Drills: Deep rein- forcement learning for logic synthesis,

    A. Hosny, S. Hashemi, M. Shalan, and S. Reda, “Drills: Deep rein- forcement learning for logic synthesis,” inProc. ASP-DAC, 2020, pp. 581–586

    2020

  5. [13]

    Flowtune: Practical multi-armed bandits in boolean optimization,

    W. Lau Netoet al., “Flowtune: Practical multi-armed bandits in boolean optimization,”IEEE Transactions on Computer-Aided Design of Inte- grated Circuits and Systems, 2022, arXiv:2202.07721

    2022 arXiv

  6. [14]

    Boils: Bayesian optimisation for logic synthesis,

    A. Grosnit, C. Malherbe, R. Tutunov, X. Wan, J. Wang, and H. Bou- Ammar, “Boils: Bayesian optimisation for logic synthesis,” inProc. DATE, 2022, pp. 1193–1196

    2022

  7. [15]

    Alphasyn: Logic synthesis optimization with efficient monte carlo tree search,

    Z. Pei, F. Liu, Z. He, G. Chen, H. Zheng, K. Zhu, and B. Yu, “Alphasyn: Logic synthesis optimization with efficient monte carlo tree search,” in Proc. ICCAD, 2023

    2023

  8. [16]

    Exploring logic optimizations with reinforcement learning and graph convolutional network,

    K. Zhu, M. Liu, H. Chen, Z. Zhao, and D. Z. Pan, “Exploring logic optimizations with reinforcement learning and graph convolutional network,” inProc. MLCAD, 2020, pp. 145–150

    2020

  9. [17]

    Retrieval-guided reinforcement learning for boolean circuit minimiza- tion,

    A. B. Chowdhury, M. Romanelli, B. Tan, R. Karri, and S. Garg, “Retrieval-guided reinforcement learning for boolean circuit minimiza- tion,” inProc. ICLR, 2024

    2024

  10. [18]

    LOSTIN: Logic optimization via spatio-temporal information with hybrid graph models,

    N. Wu, J. Lee, Y . Xie, and C. Hao, “LOSTIN: Logic optimization via spatio-temporal information with hybrid graph models,” inProc. ASAP, 2022

    2022

  11. [19]

    Gamora: Graph learning based symbolic reasoning for large-scale boolean networks,

    N. Wu, Y . Li, C. Hao, S. Dai, C. Yu, and Y . Xie, “Gamora: Graph learning based symbolic reasoning for large-scale boolean networks,” in Proc. DAC, 2023

    2023

  12. [20]

    BoolGebra: Attributed graph-learning for boolean algebraic manipulation,

    Y . Li, A. Agnesina, Y . Zhang, H. Ren, and C. Yu, “BoolGebra: Attributed graph-learning for boolean algebraic manipulation,” inProc. DATE, 2024

    2024

  13. [21]

    Lsoracle: a logic synthesis framework driven by artificial intelligence (invited paper),

    W. Lau Neto, M. Austin, S. Temple, L. Amar `u, X. Tang, and P.-E. Gaillardon, “Lsoracle: a logic synthesis framework driven by artificial intelligence (invited paper),” inProc. ICCAD, 2019

    2019

  14. [22]

    Helo: A heterogeneous logic optimization framework by hierarchical clustering and graph learning,

    Y . Pu, F. Liu, Z. He, K. Zhu, R. Fu, Z. Wang, T.-Y . Ho, and B. Yu, “Helo: A heterogeneous logic optimization framework by hierarchical clustering and graph learning,” inProc. ISPD, 2025

    2025

  15. [23]

    Dag-aware synthesis orchestration,

    Y . Li, M. Liu, H. Ren, A. Mishchenko, and C. Yu, “Dag-aware synthesis orchestration,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2024, arXiv:2310.07846

    2024 arXiv

  16. [24]

    Abc: An academic industrial-strength verification tool,

    R. Brayton and A. Mishchenko, “Abc: An academic industrial-strength verification tool,”Proc. CAV, 2010

    2010

  17. [25]

    The epfl logic synthesis libraries,

    M. Soeken, H. Riener, W. Haaswijk, E. Testa, B. Schmitz, G. Meuli, F. Mozafari, and G. De Micheli, “The epfl logic synthesis libraries,” Proc. IWLS, 2018

    2018

  18. [26]

    Provably correct peephole optimizations with alive,

    N. P. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr, “Provably correct peephole optimizations with alive,” inProc. PLDI, 2015, pp. 22–32

    2015

  19. [27]

    Alive2: Bounded translation validation for llvm,

    N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, and J. Regehr, “Alive2: Bounded translation validation for llvm,” inProc. PLDI, 2021, pp. 65–79

    2021

  20. [28]

    Mathematical discoveries from program search with large language models,

    B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont, F. J. R. Ruiz, J. S. Ellenberg, P. Wang, O. Fawzi, P. Kohli, and A. Fawzi, “Mathematical discoveries from program search with large language models,”Nature, vol. 625, pp. 468–475, 2024

    2024

  21. [29]

    Solving olympiad geometry without human demonstrations,

    T. H. Trinh, Y . Wu, Q. V . Le, H. He, and T. Luong, “Solving olympiad geometry without human demonstrations,”Nature, vol. 625, no. 7995, pp. 476–482, 2024

    2024

  22. [30]

    Provably good prim–dijkstra revisited: New theory and a practical algorithm for a classical vlsi routing problem with llms,

    K. Zhu, “Provably good prim–dijkstra revisited: New theory and a practical algorithm for a classical vlsi routing problem with llms,” 2026, arXiv:2607.17005

    2026 arXiv

  23. [31]

    Robust boolean reasoning for equivalence checking and functional property verification,

    A. Kuehlmann, V . Paruthi, F. Krohm, and M. Ganai, “Robust boolean reasoning for equivalence checking and functional property verification,” inProc. ICCAD, 2002. APPENDIX A. The discarded-cut lemma Lemma(Lemma 4, restated).Letρbe any recipe stage that invokes cut rewriting on ...

    2002

  24. [32]

    Minimum cardinality and arbitrary multi-step reachable sets lie outside this result

    At the one-recipe scope of Definition 2, aliases preserve every endpoint pointwise and Part 2 preserves the node–depth frontier across the dominance deletion. Minimum cardinality and arbitrary multi-step reachable sets lie outside this result. The two remaining look-alike pair...

  25. [33]

    reduce the one-node identitiesmaj(x, x, y) =xand maj(x,¯x, y) =y

  26. [34]

    sort fanins and structurally hash identical majority triples

  27. [35]

    delete nodes unreachable from the ordered outputs; and

  28. [36]

    No reassociation, balancing, rewriting, refactoring, resubsti- tution, or SAT sweeping occurs inN

    canonically relabel nodes by ASAP depth and then by their canonical fanin triples, preserving PI and PO order. No reassociation, balancing, rewriting, refactoring, resubsti- tution, or SAT sweeping occurs inN. The procedure is deterministic, semantics preserving, and idempoten...

    1941

  29. [37]

    The normal-effort HeLO- comparison recipe iscgo -M 2; cgo_mig; the maximum- effort recipe iscgo -M 1 -P 20; cgo_mig -R 60 -T

    Configuration and evidence contract:Table XX gives the complete configuration delta. The normal-effort HeLO- comparison recipe iscgo -M 2; cgo_mig; the maximum- effort recipe iscgo -M 1 -P 20; cgo_mig -R 60 -T

  30. [39]

    Ratios and speedups use the same inputs, host, harness, and published orchestratecommand as Tables XVII and XVIII

    Orchestration results:Table XXII reports the fast over- lay under all four published Orchestration schedules. Ratios and speedups use the same inputs, host, harness, and published orchestratecommand as Tables XVII and XVIII. In single-pass mode, the overlay moves theO 16 depth...

  31. [40]

    At normal effort, its exact-input and all-context NDP geomeans are0.940 and0.944; at maximum effort, they are0.944and0.929

    HeLO-comparison results:Table XXIII reports the two TACO-fast effort settings on the six available HeLO cases, preserving the input-fidelity groups of Table VII. At normal effort, its exact-input and all-context NDP geomeans are0.940 and0.944; at maximum effort, they are0.944a...

  32. [41]

    The eleven corrected inputs inO 16 \D 55 entered after the configuration freeze and form the disjoint evaluation subset reported above

    Scope of the fast evidence:The tuned values were selected and evaluated on the development manifests, so the D55 andH 6 results are in-sample performance evidence. The eleven corrected inputs inO 16 \D 55 entered after the configuration freeze and form the disjoint evaluation ...

    1964

  33. [1800]

    TABLE XX COMPLETE DELTA FROM TACO TO THE FAST OVERLAY

    In the released command line,-Cselects the main- paperTACOconfiguration. TABLE XX COMPLETE DELTA FROM TACO TO THE FAST OVERLAY. SettingTACO TACO-fast RF node/cone bound 10/16 9/14 RW cut keep count 250 100 Iterative stop no-improvement fixpoint fixpoint or gain<0.5% AIG yield ...

Pith tools

Reviewed July 30, 2026 · model on record in the stance chip above.