{"id":"c1461988-096b-4f70-8101-65d68d58ed75","arxiv_id":"2411.15442","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":3,"one_line_summary":"AssertCraft generates SystemVerilog assertions from specification documents using subtask decomposition, fine-tuned GPT-3.5, and iterative compiler-guided repair, reporting 7.3x more correct assertions than a plain prompt baseline.","lead":"This paper presents an LLM-based tool, AssertCraft, that turns design specification documents into SystemVerilog assertions by first decomposing the spec into comments and then fine-tuning and iteratively repairing the generated assertions. It reports large improvements over a plain GPT baseline, but the evaluation metrics and reported numbers raise questions about how the claims would hold up in practice.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The headline 7.3x claim rests on Section III-C2's 'functionally correct' definition: no counterexample in a 20-cycle bounded FPV run, with no vacuity check; vacuous or shallow-hold assertions therefore count as correct, so the central comparison is not yet supported.","rationale":"The reader's weakest_assumption is the same one I would put first: the bounded 20-cycle FPV oracle is load-bearing because all correctness counts depend on it. I considered whether the denominator mismatch (240 vs 892 generated assertions) is the more fundamental defect; it is a real confound, but a correct oracle would still be needed to interpret even normalized rates, whereas correcting the oracle would also expose whether more assertions are genuinely better. The paper is otherwise transparent about using GPT-3.5, fine-tuning data construction, and HDLBits-derived modules; there is no internal contradiction in the method itself. The problem is that the evidence type for 'functionally correct' is too weak for the strength of the claim. I therefore keep the reader's rejection: a revision with unbounded/vacuity-aware checking, per-assertion rates, and released artifacts could be publishable.","tokens_in":11392,"tokens_out":6270,"duration_ms":57684,"concrete_test":"Rerun the Table I/Fig. 2 evaluation on the same golden RTL and the same generated assertions with (a) an unbounded FPV proof (or at minimum a 200-cycle bound, plus induction where supported) and (b) a standard vacuity check that flags assertions whose antecedent is unreachable or never satisfied. Recompute the Plain/Decomposition/AssertCraft 'functionally correct' counts; if the AssertCraft count drops materially, or if the Plain-to-AssertCraft improvement ratio changes by more than 20%, the 20-cycle oracle is the load-bearing weakness and the headline claim overstates correctness.","verdict_should_be":"UNCHANGED","load_bearing_attack":"All correctness counts feeding the central claim (abstract; Fig. 2: Plain 19, Decomposition 81, AssertCraft 140; Table I) are produced by the scoreboard in Section III-C2: an assertion is 'functionally correct' if it has no syntax error and no counterexample within the 20 cycles of the FPV run. The threshold is justified only as 'sufficiently accurate in its prediction.' This is a bounded model-checking criterion, not semantic correctness against the specification. Two concrete failure modes make the concern load-bearing. First, vacuity: a property whose antecedent is not satisfiable within 20 cycles (e.g., an over-constrained or tautologically false antecedent) has no counterexample and is counted as functionally correct; the paper reports no vacuity analysis. Second, depth: several Table II designs (32-bit LFSR, 12-hour clock, Conway's Game of Life) have state spaces or initialization sequences far beyond 20 cycles; a property can hold for 20 cycles and fail later, so the bounded pass is at best partial evidence. Since every 'functionally correct' count in the 7.3x comparison is filtered through this oracle, a biased oracle directly changes the headline. The 7.3x is also partly a quantity effect: Plain GPT generates only 240 assertions vs AssertCraft's 892 (Fig. 2), so the raw-count comparison mixes increased output with improved correctness; even without that confound, the correctness definition remains the weakest load-bearing step.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents AssertCraft, a pipeline that generates SystemVerilog assertions from natural-language design specifications. The pipeline combines subtask-focused fine-tuning of GPT-3.5-turbo (first extracting FSM transitions, conditions, and variable ranges from the spec, then turning those comments into assertions) with an iterative repair loop in which a custom compiler emits structured error messages and a bug-fixing LLM corrects syntax and semantic errors. The evaluation is performed on a curated subset of HDLBits designs with golden RTL, using a scoreboard that classifies assertions as syntax-failed, functionally incorrect (counterexample found), or functionally correct (no counterexample in a 20-cycle FPV run). The paper reports a 7.3-fold increase in the number of functionally correct assertions over a plain GPT-3.5 baseline, a 26% increase in syntax-free assertions, and near-100% stimuli coverage on several design categories.","tokens_in":11667,"tokens_out":4286,"duration_ms":41713,"significance":"If the reported results hold, the work is a useful step toward automating formal property generation from specifications. The paper contributes a complete tool flow, a dataset of HDLBits-derived verification tasks, a custom compiler for assertion repair, and an evaluation scoreboard. The concrete, falsifiable headline numbers and the release-oriented dataset construction are strengths. However, the central empirical claims rest on a correctness oracle that equates bounded FPV success with functional correctness, and on a comparison that mixes output quantity with quality. These issues must be addressed before the significance of the 7.3x and 26% claims can be assessed.","major_comments":[{"comment":"The definition of 'functionally correct' is load-bearing and is not a proxy for semantic correctness. Section III-C2 labels an assertion functionally correct if it has no syntax error and no counterexample within the 20 cycles of the FPV run, and justifies this only as 'sufficiently accurate in its prediction.' This criterion counts vacuous assertions (e.g., those with unsatisfiable antecedents within 20 cycles) as correct, and it misses failures that occur after cycle 20. Several designs in Table II -- the 32-bit LFSR, the 12-hour clock, and Conway's Game of Life -- have state spaces and initialization behavior that make 20-cycle bounded checking a weak test. Because every correctness count in the abstract, Figure 2, and Table I is produced by this oracle, the central 7.3x claim is not yet supported. Please add vacuity checks, run unbounded or substantially longer FPV where possible, compare 20-cycle results against unbounded results, and manually audit a random sample of 'correct' assertions against the specifications.","section":"III-C2"},{"comment":"The 7.3x improvement is confounded by a large difference in the number of generated assertions. The plain GPT baseline produced 240 assertions total, while Decomposition GPT and AssertCraft each produced 892. The headline ratio (19 vs 140 functionally correct) therefore mixes increased output volume with improved per-assertion quality. The percentage subplot in Figure 2 shows that AssertCraft achieves 15% functionally correct versus 7% for plain GPT, which is a 2.1x quality improvement, not 7.3x. Please report per-assertion rates (correct per generated assertion), compare pipelines on a fixed generation budget or on the same set of designs, and clarify how many assertions each pipeline attempted per design.","section":"Figure 2 and Section IV-A"},{"comment":"The fine-tuning data construction and the coverage metrics lack sufficient validation for the claims made. The comment-assertion pairs are filtered by a word2vec cosine-similarity threshold of 0.6, which is presented without any sensitivity analysis, and 500 of the 1000 pairs are 'randomly generated by an automated script,' whose semantic quality is not demonstrated. Additionally, Section IV-B reports 'stimuli coverage,' 'checker coverage,' and 'formal coverage' as distributions without defining these metrics or stating the FPV coverage model used. With vacuous assertions, coverage numbers are uninterpretable. Please define the coverage metrics precisely, report the coverage engine setup, and provide a sensitivity analysis for the cosine threshold and the synthetic-data generation process.","section":"III-C1 and Section IV-B"},{"comment":"The experimental section reports single-run results with no measure of variance or statistical significance. GPT-3.5-turbo generation is stochastic, and counts such as the 7.3x ratio and the 26% syntax improvement may vary across runs and prompt orders. Please report multiple independent runs with means and ranges (or confidence intervals), and state the number of runs used for each number in Figure 2 and Table I. Without this, the precision of the headline claims is not established.","section":"Section IV"}],"minor_comments":[{"comment":"The term 'SV A' in the abstract should be 'SVA' (SystemVerilog Assertions), and the phrase 'sub-tasked focused fine-tuning' is used inconsistently with 'sub-task-focused fine-tuning' elsewhere; please standardize the terminology.","section":"Abstract and Section I"},{"comment":"The hierarchical numbering scheme for modules is introduced but never fully explained; Table II and Figure 3 use indices like '2.2.1.2' without a legend, which makes the per-module results difficult to interpret.","section":"Section III-C1"},{"comment":"The plain-GPT example in Listing 1 is cited as evidence of failure, but the response appears to contain incomplete or placeholder signal names; please clarify whether this is the raw model output and how the iterative repair would handle it.","section":"Listing 1"},{"comment":"Table I reports 'Assertions with Fixed Error' (234) and 'Assertions without errors' (294), but the relationship between these numbers and the syntax-failed count (364) is not explained; please provide a flow diagram or state which stages produce these counts.","section":"Section III-B and Table I"}],"recommendation":"major_revision","confidential_remarks":"The work is likely suitable for the journal if the evaluation is substantially strengthened. The main empirical claims are currently not supported by the 20-cycle FPV oracle and the quantity/quality confound. I recommend a major revision rather than rejection because the methodology is plausible and the issues are fixable with additional experiments and reporting. Please also ensure the dataset and code are made available to support reproducibility."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis is a plausible engineering flow for generating SystemVerilog assertions from natural-language specs, and it is the first to target raw specification documents directly rather than detailed comments or RTL. The subtask decomposition (FSM states, conditions, variable ranges via separate LLM queries), the compiler-guided iterative repair with tailored error messages, and the HDLBits-derived benchmark with golden RTL and TCL scripts are genuinely new and sensible. The fine-tuning dataset construction (GitHub scraping plus synthetic pairs) is reasonable, and the qualitative point that decomposition plus repair helps is believable.\n\nThe soft spots are serious. Section III-C2 defines the correctness oracle: an assertion is functionally correct if it has no syntax error and no counterexample within 20 FPV cycles. The threshold is justified only by the claim that it is 'sufficiently accurate,' with no supporting data. Two failure modes matter: vacuous assertions (antecedent unsatisfiable within 20 cycles) pass as correct, and for large-state designs (32-bit LFSR, 12-hour clock, Conway's Game of Life), properties can hold for 20 cycles and fail later. No vacuity check is reported. Since every count in the headline comparison passes through this filter, a biased oracle directly changes the headline. The 7.3x is also partly a quantity effect: the plain baseline generated only 240 assertions versus 892 for the full flow, so the comparison mixes more output with improved quality. The 26% improvement is also reported inconsistently—abstract says 'free from syntax errors,' conclusion says 'correct assertions,' and the contribution bullet says 'fix 26% assertions with bugs.' There is no code, data, or multiple runs, so I cannot check the numbers independently.\n\nThat said, the idea is timely and the related work is well covered. This deserves peer review, not desk rejection: a rigorous referee could push for a real semantic oracle (full proof, or at least longer bounded runs plus vacuity checking), a cleaner experimental design that controls for output count, and a public release. Who is this for? Researchers in LLM-assisted formal verification and assertion mining. It is a legitimate engineering contribution that needs hardening, not a breakthrough.\n\nMy recommendation: send it to review, expect major revision on the evaluation.","headline":"Plausible idea, weak oracle: the 7.3x correctness claim rests on a 20-cycle bounded FPV check with no vacuity analysis, so the evidence doesn't yet support the headline despite a solid engineering pipeline.","tokens_in":12206,"tokens_out":2809,"would_cite":false,"duration_ms":25061,"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":"LLM flow turns specs into Verilog assertions 7.3x more often","keywords":["SystemVerilog assertions","formal property verification","large language models","subtask fine-tuning","iterative repair","specification-to-assertion","LLM-based hardware verification","coverage analysis"],"falsifier":"Run every assertion the flow labels functionally correct through an FPV engine with a much longer time bound, such as 200 cycles, and also against several deliberately mutated RTL variants; if many assertions still pass on mutated designs, or fail only after cycle 20, the paper's correctness measure is too weak to match the intended specification.","tokens_in":11108,"feed_emoji":"⚙️","tokens_out":5706,"duration_ms":47119,"temperature":0.7,"pith_summary":"The paper claims that asking a large language model to write formal Verilog assertions directly from a design specification mostly fails, because it is a multi-step reasoning task. The authors propose AssertCraft, which splits the task into subtasks—extracting finite-state-machine transitions, conditional statements, and variable ranges from the specification text, then generating one assertion per extracted comment—and fine-tunes a GPT-3.5-based model on a comment-to-assertion dataset. A second stage feeds assertions plus a golden RTL implementation through a custom compiler whose meaningful error messages are sent back to the LLM for iterative repair. The paper reports a 7.3-fold increase in the number of functionally correct assertions and a 26% increase in syntax-free assertions over the plain GPT-3.5 baseline, with near-100% stimuli coverage on several HDLBits-based designs. The practical point: this is a step toward fully automated formal verification from specifications rather than from comments or RTL alone.","feed_headline":"LLM flow turns specs into Verilog assertions 7.3x more often","feed_subtitle":"Subtask-focused fine-tuning plus compiler-guided repair makes formal assertion generation practical.","key_machinery":"The machinery is two coupled mechanisms. First, 'subtask-focused fine-tuning': the specification-to-assertion task is split by three JSON-schema prompts—one extracts FSM states, transition conditions, and output conditions; one extracts conditional statements; one extracts variable ranges and values—and each extracted item becomes a short comment, which a GPT-3.5 model fine-tuned on a 1000-sample comment-assertion dataset (500 scraped from GitHub and filtered by word2vec cosine similarity above 0.6, 500 script-generated) turns into an assertion. Second, 'iterative repair': a custom compiler's error messages are sent back to a repair LLM in a loop, including a rule that rewrites sequential implications into combinational form, until the assertion compiles or the loop hits a threshold.","core_discovery":"The central claim is that high-quality SystemVerilog assertions can be generated automatically from natural-language design specifications by decomposing the problem into a comment-extraction subtask and a comment-to-assertion subtask, fine-tuning the LLM separately on each, and then repairing the output in a loop with a custom compiler that produces LLM-readable error messages. Under this flow, the paper reports that the number of functionally correct assertions rises from 19 with the plain GPT-3.5 baseline to 140 with the full AssertCraft flow on its 892-assertion dataset, a 7.3-fold improvement, and that iterative repair increases the number of assertions free of syntax errors by 26%. The paper also claims near-100% stimuli coverage on several designs, meaning the generated assertions exercise the design's input space broadly, although checker and formal coverage vary by design category.","pith_inferences":["The 20-cycle bound on formal verification means 'functionally correct' may count vacuous or over-constrained assertions; extending the bound or checking against mutated RTL could shrink the reported 140-assertion count.","The same subtask decomposition could transfer to other specification-to-code generation tasks, such as cover-property generation or testbench generation, since it converts an unstructured text-to-code problem into structured extraction plus per-item generation.","Making compiler diagnostics LLM-friendly, as the custom compiler does here, is a general recipe: rather than asking the model to parse raw syntax errors, the repair prompt should pinpoint the offending construct and suggest the expected form.","Because the authors chose GPT-3.5 for cost, pairing the same fine-tuned extraction and repair loop with a stronger base model could compound the gains reported here."],"forward_implications":["The subtask decomposition makes specification-to-assertion generation feasible without a large specification-assertion dataset, a practical obstacle in industrial verification.","Iterative repair with informative compiler feedback can recover 26% of assertions with syntax bugs, so generated assertions can reach usable quality without human rewrite.","The flow produces assertions with near-100% stimuli coverage on several HDLBits designs, suggesting the generated set exercises input behavior broadly.","The method applies to both sequential and combinational modules, though the paper reports more syntax failures on clock-less combinational modules.","If the flow generalizes beyond the evaluated HDLBits subset, it offers a path toward continuous formal verification during RTL development."],"supporting_citations":[{"why":"Establishes that LLMs can generate assertions from detailed comments, the baseline capability the paper extends to specification-level text.","marker":"[7]"},{"why":"Provides the prompt rules the paper adapts and the comparison point for generating assertions from RTL code.","marker":"[9]"},{"why":"Supplies the idea that decomposing a hard question into subtasks improves LLM performance, motivating the subtask-focused fine-tuning.","marker":"[13]"},{"why":"Provides the iterative multi-location repair paradigm that the paper imports into the assertion repair loop.","marker":"[18]"},{"why":"Represents the prior automated assertion-generation approach that requires simulation traces, contrasting with the spec-only generation pursued here.","marker":"[19]"},{"why":"Supplies the HDLBits designs and specifications from which the evaluation dataset is derived.","marker":"[29]"},{"why":"Supplies the golden RTL implementations used to make the designs synthesizable and compatible with FPV engines.","marker":"[30]"}],"fun_headline_variants":["Subtask fine-tuning lifts correct Verilog assertions 7.3x","Compiler-repaired LLM output: 7.3x more valid assertions","Auto SVA from specs: subtask LLM + iterative fix boosts 7.3x","LLM flow: 7.3x more correct assertions via subtask tuning","Iterative LLM prompting yields 7.3x valid Verilog assertions"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The correctness counts rest on the assumption that an assertion is functionally correct if a formal verification engine finds no counterexample within 20 clock cycles on the golden RTL; this bounded, one-implementation check could let empty or over-constrained assertions count as correct.","fun_headline_variants_meta":{"raw":{"variants":["Subtask fine-tuning lifts correct Verilog assertions 7.3x","Compiler-repaired LLM output: 7.3x more valid assertions","Auto SVA from specs: subtask LLM + iterative fix boosts 7.3x","LLM flow: 7.3x more correct assertions via subtask tuning","Iterative LLM prompting yields 7.3x valid Verilog assertions"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000623,"raw_usage":{"total_tokens":2867,"prompt_tokens":911,"completion_tokens":1956,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":527,"completion_tokens_details":{"reasoning_tokens":1851}},"tokens_in":527,"tokens_out":1956,"duration_ms":14402,"temperature":1.0,"reasoning_tokens":1851,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T14:17:13.197862+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run every assertion the flow labels functionally correct through an FPV engine with a much longer time bound, such as 200 cycles, and also against several deliberately mutated RTL variants; if many assertions still pass on mutated designs, or fail only after cycle 20, the paper's correctness measure is too weak to match the intended specification.","supporting_citations":[{"cited_title":"Iter: Iterative neural repair for multi- location patches,","cited_arxiv_id":null,"evidence_quote":"Provides the iterative multi-location repair paradigm that the paper imports into the assertion repair loop."},{"cited_title":"Goldmine: Automatic assertion generation using data mining and static analysis,","cited_arxiv_id":null,"evidence_quote":"Represents the prior automated assertion-generation approach that requires simulation traces, contrasting with the spec-only generation pursued here."},{"cited_title":"[Online]","cited_arxiv_id":null,"evidence_quote":"Supplies the HDLBits designs and specifications from which the evaluation dataset is derived."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the golden RTL implementations used to make the designs synthesizable and compatible with FPV engines."}],"review_version":1}