Pith. sign in

REVIEW 5 major objections 5 minor 51 references

A Novel Mutation Based Method for Detecting FPGA Logic Synthesis Tool Bugs

T0 review · 5 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read By mutating only dormant 'zombie' logic in Verilog, VERMEI generates behavior-preserving test programs that exposed 15 real bugs in FPGA synthesis tools.

desk verdict Useful extension of zombie-block mutation to Verilog FPGA synthesis with real vendor-confirmed bugs, but the equivalence guarantee rests on finite simulation and the paper has several reporting slips. read the letter →

arxiv 2508.15536 v1 pith:JWHQZQBC submitted 2025-08-21 cs.SE

Yi Zhang , He Jiang , Xiaochen Li , Shikai Guo , Peiyu Zou , Zun Wang This is my paper · ORCID
classification cs.SE
keywords FPGAsynthesistooltestingVerilogmutationzombielogicdifferentialequivalentvariantsBayesiansamplingcoverage-guidedEDAbugs
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

This paper tries to establish that FPGA logic synthesis tools can be tested more effectively by mutating only the parts of a Verilog program that are inactive under current stimuli, so the mutated program is supposed to be behaviorally equivalent to the original. The method, VERMEI, covers the seed design, marks untriggered 'zombie' regions, prunes or inserts complex logic fragments there, and then compares synthesized outputs of seed and mutant. A mismatch, crash, or hang under identical stimuli is counted as a synthesis tool bug. On Yosys, Vivado, and Quartus Prime, VERMEI reported 15 bugs in five months, 9 confirmed as new, and outperformed existing generators Verismith and EvoHDL in controlled bug-count and coverage comparisons. If correct, this gives a principled way to generate semantically rich but equivalent test programs that current random and template-based generators miss.

What carries the argument

The load-bearing object is 'zombie logic': Verilog code that is syntactically present but inactive under the current clock cycle and input conditions, yet may be reactivated by future signal transitions. VERMEI identifies zombie logic through simulation-based coverage analysis, then applies two mutations: pruning (deleting an AST node or subtree) and insertion (adding Bayesian-sampled logic fragments from historical designs into zombie regions). The equivalence assumption is what lets differential testing attribute any seed-versus-variant output difference to a bug in the synthesis tool rather than to the mutation itself.

What would settle it

Take a variant that VERMEI classifies as equivalent and run both seed and variant through a formal equivalence checker or exhaustive reachable-state simulation; a single counterexample input sequence would show the mutation changed behavior, meaning the differential mismatch is not evidence of a synthesis tool bug.

Watch

Extended reading notes

Core claim

VERMEI's central claim is that synthesis-tool bugs can be found by generating equivalent Verilog variants through mutation confined to zombie logic: code that is dormant under the current simulation stimuli but could be reactivated later. The preprocessing module uses coverage tools on randomized testbenches to mark these regions; the mutation module prunes or inserts fragments sampled from a large corpus of real Verilog designs using a Bayesian model; the bug identification module synthesizes seed and variants and flags any output difference. The paper reports that within five months this workflow found 15 valid bugs in the latest versions of Yosys, Vivado, and Quartus Prime, 9 confirmed as

Load-bearing premise

A mutation is truly behavior-preserving only if the identified 'zombie' region can never affect any output, but the paper infers that from finite simulation coverage rather than from a proof for all clock cycles and input-state combinations.

Editorial extensions

If this is right

  • If the equivalence guarantee holds, any seed/mutant output mismatch can be attributed to the synthesis tool, enabling bug detection on complex designs without a manually written oracle.
  • Combining pruning and insertion is load-bearing: the paper reports VERMEI detects 50.4% and 15.7% more bugs on average than prune-only and insert-only variants, so both operations contribute distinct structural diversity.
  • Bayesian-sampled insertion from real Verilog designs increases line, condition, and branch coverage over grammar-based and template-based generators, meaning the mutants explore synthesis paths that the baselines saturate on.
  • VERMEI found new bugs in current releases of both open-source and commercial synthesis tools, showing the approach remains viable even on heavily maintained FPGA toolchains.

Reading between the lines

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

  • Editorial inference: the finite-simulation coverage step cannot prove that a zombie region is inactive for every possible clock cycle and input history, so some variants classified as equivalent may not truly be equivalent; formal verification of the mutated regions would put the equivalence claim on firmer ground.
  • Editorial inference: the same zombie-logic mutation recipe could be applied to later EDA stages, such as placement-and-routing or high-level synthesis, since any tool consuming a hardware description can be differentially tested on equivalent variants.
  • Editorial inference: because the paper's RQ5 measures structural complexity (statements, variables, branches) rather than bug-triggering power directly, the Bayesian sampler's advantage over random sampling for actual bug detection is not fully established by the reported experiments.
  • Editorial inference: the claimed 100% and 60% bug-count improvements over Verismith and EvoHDL depend on the chosen one-week budget and tool versions; repeating the comparison across more versions and time budgets would show whether the advantage generalizes.
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

5 major / 5 minor

Summary. The paper presents VERMEI, a mutation-based differential testing framework for FPGA logic synthesis tools (Yosys, Vivado, Quartus). VERMEI first uses simulation and coverage analysis to identify `zombie logic` (code that is inactive under the tested stimuli), then generates `equivalent` Verilog variants by pruning or inserting logic fragments in those zombie regions, using a Bayesian sampler trained on a corpus of Verilog designs. The seed and variants are synthesized and compared; mismatches are reported as tool bugs. The paper claims that, over five months, VERMEI found 15 bugs, 9 confirmed as new, and that it outperforms Verismith and EvoHDL in bug detection (by 100% and 60%, respectively) and in structural coverage. It also reports experiments on the two mutation operators and on the Bayesian sampling strategy.

Significance. If the central equivalence guarantee holds, the paper makes a useful contribution: it reports real, vendor-confirmed bugs in mature commercial and open-source synthesis tools, provides an open-source artifact, and proposes a mutation strategy that goes beyond purely grammar-based generation. The bug reports in Table II, including distinct crash, hang, and synthesis-mismatch cases, are concrete evidence that the approach can find real defects. However, the correctness of the principal claim depends on the unproven premise that coverage-identified `zombie logic` is behaviorally inert under all possible stimuli. The paper also has internal inconsistencies in its headline bug counts and in Table IV. These issues must be resolved before the claims can be accepted as stated.

major comments (5)
  1. [Section III.A and Algorithm 2] The central equivalence guarantee is not established. Section II-B defines Dynamic Zombie Logic as logic that is inactive under the current state but may be reactivated under future signal transitions or history paths. Section III.A identifies zombie logic only through VCS coverage over a finite random testbench with a fixed clock and fixed simulation length. Algorithm 2 mutates any AST node not in the coverage set (lines 12 and 25) without distinguishing static from dynamic zombie logic, and the `VerifyFunctionality` call (line 7) is unspecified. Finite simulation cannot rule out behavioral changes under untested clock cycles or input sequences; therefore differential mismatches could be caused by the mutation itself rather than by a synthesis-tool bug. The threats section (V.A) only asserts that `extensive simulations` were performed without giving a concrete equivalence-checking proce
  2. [Abstract, RQ1 Conclusion, Table II] The confirmed-new bug count is inconsistent across the paper. The abstract and Table II report 9 confirmed new bugs, but the RQ1 conclusion (Section IV.C) states that `8 have been confirmed as new bugs`. Additionally, Table II contains two rows with status `?` (under investigation), and the abstract says `9 of which were confirmed as new` without mentioning the two undetermined cases. The authors should reconcile these numbers and clarify whether the count includes only `New` status or also `under investigation`; this affects the headline contribution.
  3. [Table IV] Table IV lists `Vivado R2020.1` twice and omits `Vivado R2023.2`, even though Section IV.F and the RQ2 setup state that four Vivado versions/two versions per tool were tested. The duplicated row makes the per-tool totals in Table IV ambiguous and undermines the RQ4 comparison. The authors should correct the table and recompute any affected statistics.
  4. [Section IV.D] The RQ2 comparison rests on a single one-week fuzzing run per tool version, reporting totals of 8 vs 4 vs 5 bugs without confidence intervals, repeated runs, or a statistical test. The claim of `100% improvement` is a ratio of small counts and could easily be affected by randomness. Given that the paper later uses Mann-Whitney U-tests and effect sizes in RQ4, similar rigor should be applied to the headline comparison, or the claim should be softened to an exploratory observation.
  5. [Section IV.G] RQ5 is close to circular. The Bayesian sampler is designed to maximize complexity-weighted selection of syntax elements, and the evaluation then measures the number of newly added statements, variables, and conditional branches in the generated variants. These metrics are immediate proxies for the objective that the sampler optimizes, so it is expected that Bayesian sampling scores higher than random selection. This does not demonstrate that the Bayesian strategy improves bug detection or semantic diversity. The evaluation should tie the sampling strategy to a downstream outcome, such as the number of unique differential behaviors or bugs triggered, or compare against a non-Bayesian complexity-aware baseline.
minor comments (5)
  1. [Section III.B] There is an unresolved cross-reference `(section??)` in the text describing Bayesian sampling; this should be fixed.
  2. [Throughout] Typos and inconsistent terminology appear repeatedly, e.g., `flolows`, `Equivanlence`, `Extenal`, `Relation Work`, `Conclustion`, `Veriolg`, and `Know` for `Known`. A careful proofread is needed.
  3. [References] Reference [39] is discussed as both `VERGEN` and `VeriGen`, but the reference entry gives author names that do not match either tool named in the text. This should be clarified or split into proper citations.
  4. [Table II and Figure 10] Several figure/table references are not fully explained. For example, Figure 10 has subfigures (a)-(e), but the text does not state which subfigure corresponds to which tool version. Also, Table II uses `TSC` without defining the acronym in the table caption.
  5. [Section IV.B] The notation for Vivado versions is inconsistent (`Vivado Rv.2023.2` in RQ1, `Vivado R2023.2` elsewhere). Standardize the version strings.

Circularity Check

1 steps flagged · score 3.0 of 10

One self-referential RQ5 evaluation; central bug-finding claims rest on external vendor reports.

  1. fitted input called prediction [Section IV.G (RQ5), using the Bayesian sampling formula in Section III.B]
    "We compute the complexity-weighted probability of occurrence for each syntax operator zi as follows: P(zi) = C(zi) · f(zi) / Σ_j C(zj) · f(zj) where C(zi) denotes the complexity weight assigned to zi, as detailed in Table I. ... we counted ... the number of newly added statements, newly introduced variables, and new conditional branches in each variant Verilog."

    The RQ5 conclusion that Bayesian sampling is more effective than random is forced by construction. The sampler's selection probability is proportional to hand-assigned complexity weights C(zi) (Table I: control structures 4, loops 5, ternary 4), and the feedback loop explicitly increases weights of structures correlated with successful mutations. RQ5 then measures exactly those complexity features — newly added statements, variables, conditional branches — as evidence of higher semantic complexity. The evaluation metric is the optimization target, so the comparison is self-referential rather than an independent validation. This does not affect the externally confirmed bug reports, but it inflates the reported effectiveness of the sampling strategy.

full rationale

The paper's central claim — VERMEI detects 15 FPGA synthesis tool bugs, 9 confirmed new — is grounded in external vendor bug reports and differential testing, not in a derivation that collapses into its inputs. The 'zombie logic' identification via VCS line coverage over finite random testbenches is a genuine soundness concern: the paper defines dynamic zombie logic as re-activatable, and finite simulation cannot guarantee that mutated regions never affect output under all clock/input sequences. However, this is an unverified empirical premise, not a circular reduction; the paper does not derive equivalence from the coverage data by equation, and it explicitly acknowledges the risk in Section V.A. There is no load-bearing self-citation chain, no uniqueness theorem imported from the authors, and no renamed known result. The one concrete circularity is RQ5: the Bayesian sampler is explicitly designed to favor high-complexity constructs via complexity weights, and RQ5 evaluates it by counting those same constructs, so that comparison is self-referential by construction. This is a secondary ablation, not the core bug-finding evidence, so the overall circularity score is modest.

Assumptions & free parameters 4 free parameters · 4 assumptions · 1 invented entities

The method depends on hand-chosen complexity weights, unquantified sampling parameters, and a coverage-based equivalence assumption that is not formally proven. The central bug-finding claim is externalized through vendor reports, but the internal evaluation depends on these free choices.

free parameters (4)
  • Complexity weights C(zi) for each syntax element = Table I manual weights (e.g., unary=1, loops=5)
    Used in P(zi) and adjusted by feedback based on synthesis outcomes; controls sampling of inserted fragments and thus the method's output.
  • Pruning/insertion probabilities pd_parent and pd_leaf = Reassigned uniformly in [0.0, 1.0] before each operation
    Stochastic decisions for whether to prune or insert at AST nodes; no fixed values are given.
  • Acceptance threshold T and sequence length L in Bayesian sampling = Not quantified; based on average/median frequency
    Threshold selects sampled operators; L terminates sampling. Missing values make replication harder and affect generated variants.
  • Number of variants per seed = 5 in RQ1/RQ2, 10 in RQ4
    Set to 5 following prior work [9], later 10 for mutation-operation experiments; affects test quantity and bug counts.
assumptions (4)
  • domain assumption Coverage-based simulation on random testbenches identifies all behaviorally inactive logic (zombie logic) that is safe to mutate.
    Preprocessing relies on VCS line coverage over random stimuli; this is finite and cannot prove inactivity across all input sequences and clock cycles, yet central equivalence depends on it. Section III.A and Section III.
  • ad hoc to paper Pruning or inserting code into zombie regions preserves semantic equivalence between seed and variant.
    The differential oracle assumes variants are equivalent; if false, mismatches are not tool bugs. VerifyFunctionality is mentioned but not formally defined. Algorithm 2, line 7.
  • domain assumption Synthesized outputs of seed and variant can be compared under the same testbench to reveal tool bugs.
    Differential testing oracle: if outputs differ, a bug exists. This assumes the only source of difference is tool behavior. Section III-C.
  • standard math Bayes' theorem applied to corpus frequencies gives a valid sampling distribution for bug-revealing logic fragments.
    The probability model is a Markov/n-gram style estimate; formulas are standard, but the connection to bug detection is empirical. Section III.B.
invented entities (1)
  • Zombie Logic (Static and Dynamic)
    purpose: Conceptual label for inactive logic regions that VERMEI is allowed to mutate; justifies equivalence-preserving mutations.
    Defined by the authors; identified through finite simulation and coverage, so no independent formal handle is provided. Section II-B.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Novel Mutation Based Method for Detecting FPGA Logic Synthesis Tool Bugs." pith.science (2026). https://pith.science/paper/JWHQZQBC

@misc{pith2026250815536,
  author       = {Pith},
  title        = {Pith review of: A Novel Mutation Based Method for Detecting FPGA Logic Synthesis Tool Bugs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JWHQZQBC}},
  note         = {Machine review of arXiv:2508.15536}
}
read the original abstract

FPGA (Field-Programmable Gate Array) logic synthesis tools are key components in the EDA (Electronic Design Automation) toolchain. They convert hardware designs written in description languages such as Verilog into gate-level representations for FPGAs. However, defects in these tools may lead to unexpected behaviors and pose security risks. Therefore, it is crucial to harden these tools through testing. Although several methods have been proposed to automatically test FPGA logic synthesis tools, the challenge remains of insufficient semantic and logical complexity in test programs. In this paper, we propose VERMEI, a new method for testing FPGA logic synthesis tools. VERMEI consists of three modules: preprocessing, equivalent mutation, and bug identification. The preprocessing module identifies zombie logic (inactive code with no impact on the circuit output) in seed programs through simulation and coverage analysis. The equivalent mutation module generates equivalent variants of seed programs by pruning or inserting logic fragments in zombie areas. It uses Bayesian sampling to extract logic fragments from historical Verilog designs, making the generated variants have complex control flows and structures. The bug identification module, based on differential testing, compares the synthesized outputs of seed and variant programs to identify bugs. Experiments on Yosys, Vivado, and Quartus demonstrate that VERMEI outperforms the state-of-the-art methods. Within five months, VERMEI reported 15 bugs to vendors, 9 of which were confirmed as new.

Figures

Figures reproduced from arXiv: 2508.15536 by the authors.

Figure 1
Figure 1. The process of FPGA logic synthesis In summary, this paper makes the following contributions: • We propose VERMEI, a novel testing method for de￾tecting bugs in FPGA logic synthesis tool. VERMEI utilizes the equivalent mutation module and the bug identification module to address the insufficient semantic logic complexity challenge in FPGA logic synthesis tool testing. • We conducted extensive experiments on Yosys, V… view at source ↗
Figure 2
Figure 2. Example module demonstrating counter behavior with [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. The framework of VERMEI Algorithm 1 VERMEI Input: Logic Synthesizer S, Verilog test program V , Testbench T Output: Reported Bugs B 1 Procedure TEST ( S, V , T): // Step 1: Extract coverage and V_Input 2 V Input ← Verilog test program V 3 Testbench T ← V Input ← random(0...N) 4 Vexe ← S.Synthesize(V, T) 5 C ← {Coverage(Vexe.Execute(i)) | i ∈ T} // Step 2: Generate equivalent variants 6 for iter ← 1 to MAX-ITER do 7 … view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: presents a concrete example that illustrates how pruning mutations operate on different parts of the Verilog seed program. In [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: TSC Yosys-#4290. Hang with feedback arcs (https://github.com/ [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]
Figure 6
Figure 6. Figure 6: TSC Yosys-#3691. Crash with flip-flop (https://github.com/YosysHQ/ [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: TSC Vivado-Rqvc2SAB. Synthesis Mismatch Due to Condi [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: Comparison of Bugs Detected by VERMEI the Baselines [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]
Figure 9
Figure 9. Figure 9: The coverage of VERMEI and the baselines on line, condition and branch. [PITH_FULL_IMAGE:figures/full_fig_p011_9.png]
Figure 10
Figure 10. Figure 10: Time spent on detecting bugs for VERMEI and its variants [PITH_FULL_IMAGE:figures/full_fig_p012_10.png]
Figure 11
Figure 11. Figure 11: The distribution of generated Verilog variants by [PITH_FULL_IMAGE:figures/full_fig_p013_11.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

51 extracted references · 45 canonical work pages

  1. [9]

    Detecting simulink compiler bugs via controllable zombie blocks mutation,

    S. Guo, H. Jiang, Z. Xu, X. Li, Z. Ren, Z. Zhou, and R. Chen, “Detecting simulink compiler bugs via controllable zombie blocks mutation,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Singapore: ACM, 2022, pp. 1061–1072

    work page 2022

  2. [1]

    A survey and perspective on artificial intelligence for security-aware electronic design automation,

    D. Koblah, R. Acharya, D. Capecci, O. Dizon-Paradis, S. Tajik, F. Ganji, D. Woodard, and D. Forte, “A survey and perspective on artificial intelligence for security-aware electronic design automation,” ACM Transactions on Design Automation of Electronic Systems, vol. 28, no. 2, pp. 1–57, 2023

    work page 2023

  3. [2]

    From high-level deep neural models to fpgas,

    H. Sharma, J. Park, D. Mahajan, E. Amaro, J. K. Kim, C. Shao, A. Mishra, and H. Esmaeilzadeh, “From high-level deep neural models to fpgas,” in 2016 49th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 2016, pp. 1–12

    work page 2016

  4. [3]

    K. Tu, X. Tang, C. Yu, L. Josipovic, and Z. Chu, Logic Synthesis , 01 2024, pp. 135–164

    work page 2024

  5. [4]

    Accelerating deep learning with the opencl platform and intel stratix 10 fpgas,

    A. Ling, D. Capalija, and G. Chiu, “Accelerating deep learning with the opencl platform and intel stratix 10 fpgas,” 2015

    work page 2015

  6. [5]

    Minimizing computation in convolutional neural networks,

    J. Cong and B. Xiao, “Minimizing computation in convolutional neural networks,” in International conference on artificial neural networks . Springer, 2014, pp. 281–290

    work page 2014

  7. [6]

    Intel corporation. intel stratix 10 mx product table,

    I. Corporation, “Intel corporation. intel stratix 10 mx product table,” Accessed: 2023. [Online]. Available: https://www.intel.com/content/ dam/www/central-libraries/us/en/documents/product-catalog.pdf

    work page 2023

  8. [7]

    Detecting c++ compiler front-end bugs via grammar mutation and differential testing,

    H. Tu, H. Jiang, Z. Zhou, Y . Tang, Z. Ren, L. Qiao, and L. Jiang, “Detecting c++ compiler front-end bugs via grammar mutation and differential testing,” IEEE Transactions on Reliability , vol. 72, no. 1, pp. 343–357, 2022

    work page 2022

Show all 51 references
  1. [8]

    Detecting compiler warning defects via diversity-guided program mutation,

    Y . Tang, H. Jiang, Z. Zhou, X. Li, Z. Ren, and W. Kong, “Detecting compiler warning defects via diversity-guided program mutation,” IEEE Transactions on Software Engineering , vol. 48, no. 11, pp. 4411–4432, 2021

    2021

  2. [10]

    Regression fuzzing for deep learning systems,

    H. You, Z. Wang, J. Chen, S. Liu, and S. Li, “Regression fuzzing for deep learning systems,” in Proceedings of the 45th International Conference on Software Engineering, ser. ICSE ’23. IEEE Press, 2023, p. 82–94. [Online]. Available: https://doi.org/10.1109/ICSE48619.2023. 00019 15

    2023

  3. [12]

    Vloghammer,

    “Vloghammer,” https://bit.ly/2kCxjO3, Accessed: 2023

    2023

  4. [13]

    Finding and understanding bugs in fpga synthesis tools,

    Y . Herklotz and J. Wickerson, “Finding and understanding bugs in fpga synthesis tools,” in Proceedings of the 2020 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays . New York, NY , USA: Association for Computing Machinery, 2020, pp. 277–287. [Online]. Avail...

    2020

  5. [14]

    A novel hdl code generator for effectively testing fpga logic synthesis compilers,

    Z. Xu, S. Guo, G. Zhao, P. Zou, X. Li, and H. Jiang, “A novel hdl code generator for effectively testing fpga logic synthesis compilers,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pp. 1–1, 2025

    2025

  6. [15]

    G. D. Hachtel and F. Somenzi, Logic synthesis and verification algo- rithms. Springer Science & Business Media, 2007

    2007

  7. [16]

    Ising-fpga: A spintronics-based recon- figurable ising model solver,

    A. Mondal and A. Srivastava, “Ising-fpga: A spintronics-based recon- figurable ising model solver,” ACM Transactions on Design Automation of Electronic Systems (TODAES) , vol. 26, no. 1, pp. 1–27, 2020

    2020

  8. [17]

    Yosys open synthesis suite,

    C. Wolf, “Yosys open synthesis suite,” 2019. [Online]. Available: https://bit.ly/2kAXg0q

    2019

  9. [18]

    Vivado design suite,

    Xilinx, “Vivado design suite,” https://bit.ly/2wZAmld, Accessed: 2024

    2024

  10. [19]

    Intel quartus,

    Intel, “Intel quartus,” https://intel.ly/2m7wbCs, Accessed: 2024

    2024

  11. [20]

    Logic synthesis meets machine learning: Trading exactness for generalization,

    S. Rai, W. L. Neto, Y . Miyasaka, X. Zhang, M. Yu, Q. Yi, M. Fujita, G. B. Manske, M. F. Pontes, L. S. da Rosa et al. , “Logic synthesis meets machine learning: Trading exactness for generalization,” in 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE). I...

    2021

  12. [21]

    A survey on reactive programming,

    E. Bainomugisha, A. L. Carreton, T. v. Cutsem, S. Mostinckx, and W. d. Meuter, “A survey on reactive programming,” ACM Computing Surveys (CSUR), vol. 45, no. 4, pp. 1–34, 2013

    2013

  13. [22]

    Vcs functional verification solution,

    Synopsys, “Vcs functional verification solution,” https://www.synopsys. com/verification/simulation/vcs.html, Accessed: 2024

    2024

  14. [23]

    Bayesian computa- tion and stochastic systems,

    J. Besag, P. Green, D. Higdon, and K. Mengersen, “Bayesian computa- tion and stochastic systems,” Statistical science, vol. 10, no. 1, pp. 3–41, 1995

    1995

  15. [24]

    Bayesian data analysis,

    J. K. Kruschke, “Bayesian data analysis,” Wiley Interdisciplinary Re- views: Cognitive Science , vol. 1, no. 5, pp. 658–676, 2010

    2010

  16. [25]

    The no-u-turn sampler: adaptively setting path lengths in hamiltonian monte carlo

    M. D. Hoffman, A. Gelman et al. , “The no-u-turn sampler: adaptively setting path lengths in hamiltonian monte carlo.” J. Mach. Learn. Res. , vol. 15, no. 1, pp. 1593–1623, 2014

    2014

  17. [26]

    Compiler validation via equivalence modulo inputs,

    V . Le, M. Afshari, and Z. Su, “Compiler validation via equivalence modulo inputs,” in Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation , ser. PLDI ’14. New York, NY , USA: Association for Computing Machinery, 2014, p. 216–226. [...

    2014

  18. [27]

    Ctos: Compiler testing for optimization sequences of llvm,

    H. Jiang, Z. Zhou, Z. Ren, J. Zhang, and X. Li, “Ctos: Compiler testing for optimization sequences of llvm,” IEEE Transactions on Software Engineering, vol. 48, no. 7, pp. 2339–2358, 2021

    2021

  19. [28]

    Llm4cbi: Taming llms to generate effective test programs for compiler bug isolation,

    H. Tu, Z. Zhou, H. Jiang, I. N. B. Yusuf, Y . Li, and L. Jiang, “Llm4cbi: Taming llms to generate effective test programs for compiler bug isolation,” arXiv preprint arXiv:2307.00593 , vol. abs/2307.00593, pp. 1–16, 2023

    2023 arXiv

  20. [29]

    ece.utexas.edu/∼patt/10s.382N/handouts/vcs.pdf

    VCS User Guide, University of Texas, ” ” Accessed: 2023, https://users. ece.utexas.edu/∼patt/10s.382N/handouts/vcs.pdf

    2023

  21. [30]

    Covered: Verilog code coverage analyzer,

    T. Williams, “Covered: Verilog code coverage analyzer,” https://covered. sourceforge.net, 2010

    2010

  22. [31]

    Compiler test-program generation via memoized configuration search,

    J. Chen, C. Suo, J. Jiang, P. Chen, and X. Li, “Compiler test-program generation via memoized configuration search,” inProc. IEEE/ACM 45th Int. Conf. Softw. Eng. , 2023, pp. 2035–2047

    2023

  23. [32]

    Compiler fuzzing through deep learning,

    C. Cummins, P. Petoumenos, Z. Wang, and H. Leather, “Compiler fuzzing through deep learning,” in Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2018, pp. 95–105

    2018

  24. [33]

    Occom: efficient computation of observability-based code coverage metrics for functional verification,

    F. Fallah, S. Devadas, and K. Keutzer, “Occom: efficient computation of observability-based code coverage metrics for functional verification,” in Proceedings of the 35th Annual Design Automation Conference , ser. DAC ’98. New York, NY , USA: Association for Computing Machiner...

    1998

  25. [34]

    Finding and analyzing compiler warning defects,

    C. Sun, V . Le, and Z. Su, “Finding and analyzing compiler warning defects,” in Proc. IEEE/ACM 38th Int. Conf. Softw. Eng. , 2016, pp. 203–213

    2016

  26. [35]

    Ammann and J

    P. Ammann and J. Offutt, Introduction to Software Testing. New York, NY , USA: Cambridge University Press, 2008

    2008

  27. [36]

    A practical guide for using statistical tests to assess randomized algorithms in software engineering,

    A. Arcuri and L. C. Briand, “A practical guide for using statistical tests to assess randomized algorithms in software engineering,” in Proceedings of the 33rd International Conference on Software Engineering (ICSE) . New York, NY , USA: Association for Computing Machinery, 20...

    2011

  28. [37]

    A practical guide for using statistical tests to assess randomized algorithms in software engineering,

    A. Arcuri and L. Briand, “A practical guide for using statistical tests to assess randomized algorithms in software engineering,” in Proceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. New York, NY , USA: Association for Computing Machinery...

    2011

  29. [38]

    Locseq: Automated localization for compiler optimization sequence bugs of llvm,

    Z. Zhou, H. Jiang, Z. Ren, Y . Chen, and L. Qiao, “Locseq: Automated localization for compiler optimization sequence bugs of llvm,” IEEE Transactions on Reliability , vol. 71, no. 2, pp. 896–910, 2022

    2022

  30. [39]

    A correct- ness verification technique for commercial fpga synthesis tools,

    E.-S. Kim, J. Yoo, J.-G. Choi, J.-Y . Kim, and J.-S. Lee, “A correct- ness verification technique for commercial fpga synthesis tools,” in Proceedings of the 2nd International Workshop on Assurance Cases for Software-intensive Systems (ASSURE 2014) . Naples, Italy: IEEE, 2014,...

    2014

  31. [40]

    Betterv: controlled verilog generation with discriminative guidance,

    Z. Pei, H.-L. Zhen, M. Yuan, Y . Huang, and B. Yu, “Betterv: controlled verilog generation with discriminative guidance,” in Proceedings of the 41st International Conference on Machine Learning , ser. ICML’24. JMLR.org, 2024

    2024

  32. [41]

    Deloso: Detecting logic synthesis optimization faults based on configuration diversity,

    H. Jiang, P. Zou, X. Li, Z. Zhou, X. Zhao, Y . Zhang, and S. Guo, “Deloso: Detecting logic synthesis optimization faults based on configuration diversity,”ACM Trans. Des. Autom. Electron. Syst., vol. 30, no. 1, Dec. 2024. [Online]. Available: https://doi.org/10.1145/3701232

    2024 doi

  33. [42]

    Resource sharing for verified high-level synthesis,

    M. Pardalos, Y . Herklotz, and J. Wickerson, “Resource sharing for verified high-level synthesis,” in 2022 IEEE 30th Annual Interna- tional Symposium on Field-Programmable Custom Computing Machines (FCCM), 2022, pp. 1–6

    2022

  34. [43]

    A testing program and pragma combination selection based framework for high-level synthesis tool pragma-related bug detection,

    H. Jiang, Z. Wang, Z. Zhou, X. Li, S. Guo, W. Sun, and T. Zhang, “A testing program and pragma combination selection based framework for high-level synthesis tool pragma-related bug detection,” IEEE Transac- tions on Software Engineering , vol. 50, no. 4, pp. 937–955, 2024

    2024

  35. [44]

    Differential testing for software,

    W. M. McKeeman, “Differential testing for software,” Digital Technical Journal, vol. 10, no. 1, pp. 100–107, 1998

    1998

  36. [45]

    Difuzzrtl: Differential fuzz testing to find cpu bugs,

    J. Hur, S. Song, D. Kwon, E. Baek, J. Kim, and B. Lee, “Difuzzrtl: Differential fuzz testing to find cpu bugs,” in 2021 IEEE Symposium on Security and Privacy (SP) , 2021, pp. 1286–1303

    2021

  37. [46]

    Using sat for combinational equivalence checking,

    E. Goldberg, M. Prasad, and R. Brayton, “Using sat for combinational equivalence checking,” in Proceedings of the Conference on Design, Automation and Test in Europe , ser. DATE ’01. IEEE Press, 2001, p. 114–121

    2001

  38. [47]

    An equivalence- checking method for scheduling verification in high-level synthesis,

    C. Karfa, D. Sarkar, C. Mandal, and P. Kumar, “An equivalence- checking method for scheduling verification in high-level synthesis,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 3, pp. 556–569, 2008

    2008

  39. [48]

    Practical, low-effort equivalence verification of real code,

    D. A. Ramos and D. R. Engler, “Practical, low-effort equivalence verification of real code,” in Proceedings of the 23rd International Conference on Computer Aided Verification , ser. CA V’11. Berlin, Heidelberg: Springer-Verlag, 2011, p. 669–685

    2011

  40. [49]

    Molitor and J

    P. Molitor and J. Mohnke, Equivalence checking of digital circuits: fundamentals, principles, methods. Springer Science & Business Media, 2007

    2007

  41. [50]

    Verify: A program for proving correctness of digital hardware designs,

    H. G. Barrow, “Verify: A program for proving correctness of digital hardware designs,” Artificial Intelligence, vol. 24, no. 1-3, pp. 437–491, 1984

    1984

  42. [51]

    Conformal equivalence checker,

    Cadence, “Conformal equivalence checker,” https://bit.ly/2mkp0aa, Ac- cessed: 2024

    2024

  43. [52]

    Formality equivalence checking,

    Synopsys, “Formality equivalence checking,” https: //www.synopsys.com/implementation-and-signoff/signoff/ formality-equivalencechecking.html, Accessed: 2024

    2024

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.