REVIEW 4 major objections 4 minor 30 references
Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting
T0 review · 4 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash
Pith's one-line read LLM flow turns specs into Verilog assertions 7.3x more often
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [III-C2] 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.
- [Figure 2 and Section IV-A] 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.
- [III-C1 and Section IV-B] 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 IV] 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.
minor comments (4)
- [Abstract and Section I] 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 III-C1] 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.
- [Listing 1] 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 III-B and Table I] 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.
Circularity Check
No significant circularity: the 7.3x and 26% results are count ratios produced by an explicit, externally grounded FPV scoreboard, not conclusions forced by construction or by self-citation.
full rationale
The paper's central claims are empirical comparisons among three LLM pipelines (Plain GPT, Decomposition GPT, and the full AssertCraft flow). The headline 7.3x and 26% numbers are arithmetic outcomes of counts produced by the scoreboard described in Section III-C2, which labels an assertion 'functionally correct' when it has no syntax error and no counterexample within a 20-cycle FPV run on the golden RTL. This is an evaluation definition, not a derivation that assumes its own conclusion: the golden RTL is taken from external HDLBits solutions rather than generated by the proposed method, and the same scoring rule is applied to all compared pipelines. No load-bearing self-citation appears in the argument: references to prior assertion-generation work are external, and no uniqueness theorem or modeling ansatz is imported from the authors' own prior publications. The bounded 20-cycle window and the absence of a vacuity check are legitimate threats to the validity of 'functionally correct' as a measure of specification compliance, but they are concerns about the soundness of the evaluation oracle, not circularity in the derivation chain. Accordingly, no circular step satisfying the quoted-evidence test is present.
Assumptions & free parameters
free parameters (3)
- FPV cycle bound =
20
- Cosine similarity threshold =
0.6
- Fine-tuning epochs =
3
assumptions (3)
- domain assumption The HDLBits golden RTL implementations are functionally correct and match the corresponding specifications.
- ad hoc to paper Absence of a counterexample within 20 FPV cycles is a sufficient test for functional correctness of an assertion.
- ad hoc to paper Cosine similarity of word2vec vectors with a threshold of 0.6 reliably matches comments to assertions for the fine-tuning dataset.
Cite this review
Pith. "Pith review of Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting." pith.science (2026). https://pith.science/paper/SHGOMNCF
@misc{pith2026241115442,
author = {Pith},
title = {Pith review of: Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting},
year = {2026},
howpublished = {\url{https://pith.science/paper/SHGOMNCF}},
note = {Machine review of arXiv:2411.15442}
}
read the original abstract
Formal Property Verification (FPV), using SystemVerilog Assertions (SVA), is crucial for ensuring the completeness of design with respect to the specification. However, writing SVA is a laborious task and has a steep learning curve. In this work, we present a large language model (LLM) -based flow to automatically generate high-quality SVA from the design specification documents, named \ToolName. We introduce a novel sub-task-focused fine-tuning approach that effectively addresses functionally incorrect assertions produced by baseline LLMs, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Recognizing the prevalence of syntax and semantic errors, we also developed an iterative refinement method that enhances the LLM's initial outputs by systematically re-prompting it to correct identified issues. This process is further strengthened by a custom compiler that generates meaningful error messages, guiding the LLM towards improved accuracy. The experiments demonstrate a 26\% increase in the number of assertions free from syntax errors using this approach, showcasing its potential to streamline the FPV process.
Figures
Reference graph
Works this paper leans on
-
[1]
Autocc: Automatic discovery of covert channels in time-shared hardware,
M. Orenes-Vera, H. Yun, N. Wistoff, G. Heiser, L. Benini, D. Wentzlaff, and M. Martonosi, “Autocc: Automatic discovery of covert channels in time-shared hardware,” in Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture , 2023, pp. 871–885
work page 2023
-
[2]
Ieee standard for systemverilog–unified hardware design, specification, and verification language,
“Ieee standard for systemverilog–unified hardware design, specification, and verification language,” IEEE Std 1800-2012 (Revision of IEEE Std 1800-2009), pp. 1–1315, 2013
work page 2012
-
[3]
E. Seligman, T. Schubert, and M. A. K. Kumar, Formal verification: an essential toolkit for modern VLSI design . Elsevier, 2023
work page 2023
-
[4]
Au- tosva: Democratizing formal verification of rtl module interactions,
M. Orenes-Vera, A. Manocha, D. Wentzlaff, and M. Martonosi, “Au- tosva: Democratizing formal verification of rtl module interactions,” in 2021 58th ACM/IEEE Design Automation Conference (DAC) . IEEE, 2021, pp. 535–540
work page 2021
-
[5]
Instruction-level abstraction (ila) a uniform specification for system-on-chip (soc) verification,
B.-Y . Huang, H. Zhang, P. Subramanyan, Y . Vizel, A. Gupta, and S. Malik, “Instruction-level abstraction (ila) a uniform specification for system-on-chip (soc) verification,” ACM Transactions on Design Automation of Electronic Systems (TODAES) , vol. 24, no. 1, pp. 1–24, 2018
work page 2018
-
[6]
Software testing with large language models: Survey, landscape, and vision,
J. Wang, Y . Huang, C. Chen, Z. Liu, S. Wang, and Q. Wang, “Software testing with large language models: Survey, landscape, and vision,”IEEE Transactions on Software Engineering , 2024
2024
-
[7]
Llm-assisted generation of hardware assertions,
R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “Llm-assisted generation of hardware assertions,” arXiv preprint arXiv:2306.14027, 2023
arXiv 2023
-
[8]
(security) assertions by large language models,
——, “(security) assertions by large language models,” IEEE Transac- tions on Information Forensics and Security , 2024
work page 2024
Show all 30 references
-
[9]
Using llms to facilitate formal verification of rtl,
M. Orenes-Vera, M. Martonosi, and D. Wentzlaff, “Using llms to facilitate formal verification of rtl,”arXiv e-prints, pp. arXiv–2309, 2023
2023
-
[10]
olmpics-on what language model pre-training captures,
A. Talmor, Y . Elazar, Y . Goldberg, and J. Berant, “olmpics-on what language model pre-training captures,” Transactions of the Association for Computational Linguistics , vol. 8, pp. 743–758, 2020
2020
-
[11]
Are pretrained language models symbolic reasoners over knowledge?
N. Kassner, B. Krojer, and H. Sch ¨utze, “Are pretrained language models symbolic reasoners over knowledge?” arXiv preprint arXiv:2006.10413, 2020
2006 arXiv
-
[12]
Scaling language models: Methods, analysis & insights from training gopher,
J. W. Rae, S. Borgeaud, T. Cai, K. Millican, J. Hoffmann, F. Song, J. Aslanides, S. Henderson, R. Ring, S. Young et al., “Scaling language models: Methods, analysis & insights from training gopher,” arXiv preprint arXiv:2112.11446, 2021
2021 arXiv
-
[13]
Multi-hop reading comprehension through question decomposition and rescoring,
S. Min, V . Zhong, L. Zettlemoyer, and H. Hajishirzi, “Multi-hop reading comprehension through question decomposition and rescoring,” arXiv preprint arXiv:1906.02916, 2019
1906 arXiv
-
[14]
Formal hardware verification with bdds: An introduction,
A. J. Hu, “Formal hardware verification with bdds: An introduction,” in 1997 IEEE Pacific Rim Conference on Communications, Computers and Signal Processing, PACRIM. 10 Years Networking the Pacific Rim, 1987-1997, vol. 2. IEEE, 1997, pp. 677–682
1997
-
[15]
Formal verification in hardware design: a survey,
C. Kern and M. R. Greenstreet, “Formal verification in hardware design: a survey,” ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 4, no. 2, pp. 123–193, 1999
1999
-
[16]
Less training, more repairing please: revisiting automated program repair via zero-shot learning,
C. S. Xia and L. Zhang, “Less training, more repairing please: revisiting automated program repair via zero-shot learning,” in Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2022, pp. 959– 971
2022
-
[17]
A syntax-guided edit decoder for neural program repair,
Q. Zhu, Z. Sun, Y .-a. Xiao, W. Zhang, K. Yuan, Y . Xiong, and L. Zhang, “A syntax-guided edit decoder for neural program repair,” inProceedings of the 29th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering ,...
2021
-
[18]
Iter: Iterative neural repair for multi- location patches,
H. Ye and M. Monperrus, “Iter: Iterative neural repair for multi- location patches,” in Proceedings of the 46th IEEE/ACM International Conference on Software Engineering , 2024, pp. 1–13
2024
-
[19]
Goldmine: Automatic assertion generation using data mining and static analysis,
S. Vasudevan, D. Sheridan, S. Patel, D. Tcheng, B. Tuohy, and D. John- son, “Goldmine: Automatic assertion generation using data mining and static analysis,” in 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010) . IEEE, 2010, pp. 626–629
2010
-
[20]
Automatic genera- tion of assertions from system level design using data mining,
L. Liu, D. Sheridan, V . Athavale, and S. Vasudevan, “Automatic genera- tion of assertions from system level design using data mining,” in Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011) . IEEE, 2011, pp. 191–200
2011
-
[21]
Word level feature discovery to enhance quality of assertion mining,
L. Liu, C.-H. Lin, and S. Vasudevan, “Word level feature discovery to enhance quality of assertion mining,” in Proceedings of the International Conference on Computer-Aided Design , 2012, pp. 210–217
2012
-
[22]
A survey on assertion- based hardware verification,
H. Witharana, Y . Lyu, S. Charles, and P. Mishra, “A survey on assertion- based hardware verification,” ACM Computing Surveys (CSUR), vol. 54, no. 11s, pp. 1–33, 2022
2022
-
[23]
Verigen: A large language model for verilog code generation,
S. Thakur, B. Ahmad, H. Pearce, B. Tan, B. Dolan-Gavitt, R. Karri, and S. Garg, “Verigen: A large language model for verilog code generation,” ACM Transactions on Design Automation of Electronic Systems, vol. 29, no. 3, pp. 1–31, 2024
2024
-
[24]
GitHub Copilot · Your AI pair programmer,
GitHub, “GitHub Copilot · Your AI pair programmer,” 2021, available at https://copilot.github.com/
2021
-
[25]
Dave: Deriving automatically verilog from english,
H. Pearce, B. Tan, and R. Karri, “Dave: Deriving automatically verilog from english,” in Proceedings of the 2020 ACM/IEEE Workshop on Machine Learning for CAD , 2020, pp. 27–32
2020
-
[26]
(2022, Nov.) Introducing chatgpt
OpenAI. (2022, Nov.) Introducing chatgpt. Available at https://openai.com/blog/chatgpt
2022
-
[27]
(2023, Mar.) GPT-4
——. (2023, Mar.) GPT-4. Available at https://openai.com/research/gpt- 4
2023
-
[28]
Systemverilog assertions (sva),
M.-H. Wang, “Systemverilog assertions (sva),” COEN 207 SoC (System- on-Chip) Verification, n.d., department of Computer Engineering, Santa Clara University
-
[29]
[Online]
Problem sets - hdlbits. [Online]. Available: https://hdlbits.01xz.net/wiki/Problem
-
[30]
J. Li. Solutions to hdlbits verilog sets. Available at https://github.com/jerrylioon/Solutions-to-HDLbits-Verilog-sets
Reviewed August 12, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.