{"id":"a5ec76fe-95aa-455e-aa0b-ed7b5c4346ab","arxiv_id":"2508.15536","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"VERMEI mutates only inactive Verilog logic and uses differential testing to find 15 FPGA synthesis tool bugs, 9 newly confirmed.","lead":"This paper introduces VERMEI, a tool that rewrites inactive parts of Verilog designs and compares how FPGA synthesis tools process the original versus rewritten versions to expose tool bugs. Running against Yosys, Vivado, and Quartus, it reported 15 bugs, with 9 confirmed as new by developers.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper's core premise—that coverage-identified 'zombie logic' is behaviorally inert—is not established; finite random simulation cannot guarantee that mutated regions never affect output, so differential mismatches may reflect mutation-induced semantic changes rather than synthesis-tool bugs.","rationale":"After full-text review, the central claim—VERMEI generates semantically equivalent variants and thus differential mismatches indicate tool bugs—depends on the soundness of zombie-logic identification. The paper's own definition of dynamic zombie logic (Section II-B) admits regions that are inactive under some states but re-activatable; the preprocessing (Section III.A) uses finite random simulation with VCS, which can only establish non-execution for the sampled stimuli, not unreachability. Algorithm 2 then mutates all uncovered nodes. This is a genuine unsoundness, not merely a consensus disagreement. External vendor confirmations of 9 bugs provide some empirical support, but they do not validate the equivalence premise; a non-equivalent variant can produce a mismatch even when the tool is correct. The reader's weakest_assumption matches this concern. The proposed concrete test—formal equivalence checking of the actual bug-triggering pairs—would settle whether the concern affects the reported results. Other issues (small bug counts in RQ2, the 8-vs-9 confirmed-bug inconsistency between the abstract and RQ1 conclusion) are secondary. Therefore I agree with the CONDITIONAL verdict: the method is plausible but requires strengthening the equivalence validation before the bug-detection numbers can be fully credited.","tokens_in":21265,"tokens_out":7255,"duration_ms":75478,"concrete_test":"Reproduce VERMEI from the Figshare artifact and obtain the 15 variant/seed pairs from Table II. Run a formal sequential equivalence check on each pair (e.g., SymbiYosys `equiv_induction` or `bmc` with depth exceeding the testbench simulation length, or ABC equivalence after `prep -flatten`). If any pair is proven non-equivalent, the differential mismatch is explainable by the mutation, so that bug report is not valid evidence of a synthesis-tool defect. If all 15 are equivalent, the central premise is supported for the reported bugs.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing premise is that coverage-identified zombie logic is behaviorally inert, so mutations preserve semantics. Section III.A identifies zombie logic using VCS line coverage over a finite random testbench (fixed clock, random inputs, fixed simulation length). But Section II-B defines Dynamic Zombie Logic as logic inactive in the current state yet re-activatable under future signal transitions or history paths. Finite simulation cannot establish that an uncovered statement is unreachable across all cycles/input sequences. Algorithm 2 (PruneVisit/InsertVisit) mutates any AST node not in coverage set C without distinguishing static from dynamic zombie logic. No formal equivalence check (e.g., SAT/BMC equivalence) is reported; the 'VerifyFunctionality' step in Algorithm 2 is unspecified. Consequently, pruned/inserted fragments can alter behavior under untested stimuli, making differential mismatches potentially artifacts of the mutation rather than synthesis-tool bugs. The paper's own threats section (V.A) only asserts 'extensive simulations and validate against benchmark designs' without specifics. Since the 15 reported bugs include 4 known and 2 under investigation, and no evidence that triggering variants were equivalence-checked, the central claim that VERMEI detects 'equivalent variants' is unsubstantiated.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":21662,"tokens_out":3566,"duration_ms":41269,"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":[{"comment":"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","section":"Section III.A and Algorithm 2"},{"comment":"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.","section":"Abstract, RQ1 Conclusion, Table II"},{"comment":"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.","section":"Table IV"},{"comment":"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.","section":"Section IV.D"},{"comment":"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.","section":"Section IV.G"}],"minor_comments":[{"comment":"There is an unresolved cross-reference `(section??)` in the text describing Bayesian sampling; this should be fixed.","section":"Section III.B"},{"comment":"Typos and inconsistent terminology appear repeatedly, e.g., `flolows`, `Equivanlence`, `Extenal`, `Relation Work`, `Conclustion`, `Veriolg`, and `Know` for `Known`. A careful proofread is needed.","section":"Throughout"},{"comment":"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.","section":"References"},{"comment":"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.","section":"Table II and Figure 10"},{"comment":"The notation for Vivado versions is inconsistent (`Vivado Rv.2023.2` in RQ1, `Vivado R2023.2` elsewhere). Standardize the version strings.","section":"Section IV.B"}],"recommendation":"major_revision","confidential_remarks":"The paper reports real vendor-confirmed bugs, which is valuable, but the main methodological weakness is the lack of a formal or even bounded equivalence check for the mutated variants. The internal count inconsistencies and the duplicated row in Table IV suggest the manuscript needs careful verification before acceptance. If the authors can demonstrate that the triggering variants are semantically equivalent to their seeds (e.g., by adding a SAT/BMC equivalence check on minimized reproducers) and correct the reporting errors, the paper could become acceptable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know before you decide whether to read it. The vendor-confirmed bug list is the real content: 15 bugs reported, 9 confirmed new, across Yosys, Vivado, and Quartus. That is meaningful empirical evidence that the method finds genuine synthesis-tool defects. The second thing is that the \"equivalent variants\" claim, which the method leans on, is not actually established. Zombie logic is identified by finite random simulation, and the paper itself defines dynamic zombie logic as potentially re-activatable. So coverage cannot guarantee that mutated regions never affect behavior under untested stimuli.\n\nWhat is new: the same group published zombie-block mutation for Simulink [9], so the core mutation idea is an extension rather than a breakthrough. But applying it to Verilog FPGA synthesis, adding coverage-based zombie detection, and using a Bayesian sampler over 24k mined Verilog designs is a legitimate and reasonably engineered step. The code and data are on Figshare, and the bug reports are concrete. The comparisons against Verismith and EvoHDL are credible in direction, and the coverage improvements are plausible.\n\nSoft spots: the load-bearing premise is shaky. Algorithm 2 mutates any node not in coverage without distinguishing static from dynamic zombie logic, and the VerifyFunctionality step is unspecified. The internal threats section (V.A) only says \"extensive simulations\" without specifics, which is not enough. So a differential mismatch on a non-equivalent variant is not by itself evidence of a synthesis bug. The vendor confirmations rescue the headline, but the paper should state whether triggering variants were equivalence-checked, and if not, say so.\n\nThere are also smaller report problems: the abstract says 9 new bugs but RQ1's conclusion says 8; Table IV lists Vivado R2020.1 twice and drops R2023.2; RQ5 measures added statements/variables/branches, which is precisely what the complexity-weighted Bayesian sampler was designed to maximize, so that comparison is circular. The headline \"100% improvement\" is 8 vs 4 bugs in one-week runs with no confidence intervals or statistical test.\n\nWho it's for: people working on compiler testing, especially EDA/HDL tools. Not a theoretical contribution, but a solid empirical one with a fixable methodological gap. I'd give it a serious referee; the findings deserve scrutiny and the equivalence question can be answered with additional validation. Recommend peer review with expected major revisions.","headline":"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.","tokens_in":22079,"tokens_out":4749,"would_cite":true,"duration_ms":49579,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"By mutating only dormant 'zombie' logic in Verilog, VERMEI generates behavior-preserving test programs that exposed 15 real bugs in FPGA synthesis tools.","keywords":["FPGA synthesis tool testing","Verilog mutation","zombie logic","differential testing","equivalent variants","Bayesian sampling","coverage-guided testing","EDA tool bugs"],"falsifier":"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.","tokens_in":21214,"feed_emoji":"🐛","tokens_out":5518,"duration_ms":60271,"temperature":0.7,"pith_summary":"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.","feed_headline":"Zombie Verilog logic exposes 15 FPGA synthesis bugs","feed_subtitle":"Mutating only dormant code keeps test programs equivalent, so mismatches point to real tool defects.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Verismith, the grammar-based Verilog generator used both as the main baseline and as the source of seed programs for VERMEI.","marker":"[13]"},{"why":"EvoHDL, the template-based HDL generator used as the second baseline for bug detection and coverage comparisons.","marker":"[14]"},{"why":"Prior zombie-block mutation work in Simulink compiler testing, which VERMEI adapts to Verilog logic synthesis tools.","marker":"[9]"},{"why":"VCS, the commercial simulator whose coverage output is used to identify and annotate zombie logic in seed programs.","marker":"[22]"},{"why":"Covered, the open-source Verilog coverage analyzer used to measure line, condition, and branch coverage in the evaluation.","marker":"[30]"},{"why":"Equivalence-modulo-inputs methodology, referenced to justify the controlled random reassignment of pruning probabilities during mutation.","marker":"[26]"}],"fun_headline_variants":["Zombie logic mutations expose 15 FPGA synthesis bugs","Mutating dormant Verilog reveals 15 FPGA tool synthesis bugs","Zombie-code mutation tricks FPGA tools into exposing their bugs","Differential testing on zombie Verilog finds 15 synthesis bugs","Pruning dead logic in Verilog uncovers 15 tool bugs"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Zombie logic mutations expose 15 FPGA synthesis bugs","Mutating dormant Verilog reveals 15 FPGA tool synthesis bugs","Zombie-code mutation tricks FPGA tools into exposing their bugs","Differential testing on zombie Verilog finds 15 synthesis bugs","Pruning dead logic in Verilog uncovers 15 tool bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000821,"raw_usage":{"total_tokens":3444,"prompt_tokens":774,"completion_tokens":2670,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":518,"completion_tokens_details":{"reasoning_tokens":2584}},"tokens_in":518,"tokens_out":2670,"duration_ms":20314,"temperature":1.0,"reasoning_tokens":2584,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T17:49:52.525369+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"A novel hdl code generator for effectively testing fpga logic synthesis compilers,","cited_arxiv_id":null,"evidence_quote":"EvoHDL, the template-based HDL generator used as the second baseline for bug detection and coverage comparisons."},{"cited_title":"Detecting simulink compiler bugs via controllable zombie blocks mutation,","cited_arxiv_id":null,"evidence_quote":"Prior zombie-block mutation work in Simulink compiler testing, which VERMEI adapts to Verilog logic synthesis tools."},{"cited_title":"Vcs functional verification solution,","cited_arxiv_id":null,"evidence_quote":"VCS, the commercial simulator whose coverage output is used to identify and annotate zombie logic in seed programs."},{"cited_title":"Covered: Verilog code coverage analyzer,","cited_arxiv_id":null,"evidence_quote":"Covered, the open-source Verilog coverage analyzer used to measure line, condition, and branch coverage in the evaluation."}],"review_version":1}