Pith. sign in

REVIEW 3 major objections 6 minor 18 references

LLM-Generated Chip Assertions Need Six Fixes Before They're Trustworthy

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · glm-5.2

2026-07-09 10:30 UTC pith:ALQV7NTA

load-bearing objection A competent review of LLM-based SVA generation with useful case studies, but one causal claim about vacuity and coverage is unsupported, and none of the proposed guidelines are validated. the 3 major comments →

arxiv 2607.07444 v1 pith:ALQV7NTA submitted 2026-07-08 cs.ET

LLM Assisted Verification Assertion Generation: Challenges and Future Directions

Bhabesh Mali , Chandan Karfa This is my paper
classification cs.ET
keywords SystemVerilog AssertionsLLM-based verificationassertion-based verificationformal property verificationvacuity analysiscoverage metricssignal mappingknowledge graph
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

This paper argues that using large language models to automatically generate SystemVerilog Assertions (SVAs) for hardware verification is promising but currently unreliable, and identifies six specific challenges that must be solved to make the output systematic and quality-aware. The authors survey existing frameworks and run small case studies to show that current methods produce assertions that are vacuously provable, use nonexistent signals, fail to cover real functionality, and lack any redundancy or quality analysis. They propose a pipeline where assertions are generated from structured design specifications rather than RTL code, refined through formal-verification-tool feedback loops, evaluated using vacuity and cone-of-influence metrics beyond standard coverage numbers, and pruned of redundant or logically weak assertions to produce a compact, high-quality set.

Core claim

The central finding is that standard coverage metrics (formal coverage, branch coverage, toggle coverage) are insufficient to judge assertion quality because signal-name mismatches between LLM-generated assertions and RTL can cause assertions to be proven vacuously, falsely inflating coverage numbers. In the authors' case studies, vacuity rates of 21-36% were observed in assertions from two state-of-the-art frameworks, meaning a substantial fraction of 'proven' assertions were actually checking nothing. The paper also demonstrates that one-shot LLM generation methods produce syntactically and semantically correct assertions only about 11% of the time, while formal-tool-guided rectificationLo

What carries the argument

The central mechanism is a proposed pipeline with six components: (1) specification-driven assertion generation using structured representations like knowledge graphs rather than raw RTL, (2) mandatory signal mapping to ensure assertion signals match RTL declarations, (3) formal-verification-tool-guided rectification loops that feed error logs back to the LLM for iterative refinement, (4) vacuity analysis to detect assertions whose antecedents never activate, (5) cone-of-influence-based importance analysis to prioritize functionally significant assertions, and (6) redundancy removal through equivalence checking and strong/weak assertion comparison to reduce the final set without losing覆盖.

Load-bearing premise

The paper draws its guidelines from case studies on very small designs (a 4-bit ripple-carry adder, I2C, UART, and a small GA_68 design), and it is not established whether the observed vacuity rates, signal mismatch patterns, or the effectiveness of the proposed rectification loops would generalize to industrial-scale hardware designs with specifications and RTL that are orders of magnitude larger.

What would settle it

The paper's claims would be weakened if a larger-scale study found that vacuity rates from current frameworks are much lower on industrial designs, or if one-shot generation methods performed comparably to rectification-loop methods when evaluated on larger, more complex IPs. The central recommendation that assertions must come from specifications rather than RTL would also be challenged if RTL-derived assertions were shown to catch a distinct class of bugs that specification-derived assertions systematically miss.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the proposed pipeline is adopted, formal verification teams could replace manual assertion writing with LLM-assisted generation that includes built-in quality gates, potentially reducing the 50-60% of chip design time currently spent on verification.
  • The vacuity analysis recommendation means that existing coverage reports from current LLM-based assertion frameworks may be significantly overstating their effectiveness, and teams using these tools should audit for vacuous proofs before trusting coverage numbers.
  • The shift from RTL-derived to specification-derived assertions changes the verification paradigm: assertions would check whether the implementation matches design intent rather than whether the implementation matches itself, which is the correct semantic for formal property verification.
  • The recommendation to use signal-wise knowledge graph representations for long specifications suggests that scaling LLM-based assertion generation to industrial-size IPs will require graph-structured retrieval rather than monolithic prompting.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. This paper reviews recent LLM-based SystemVerilog Assertion (SVA) generation frameworks and identifies six challenges: specification-vs-RTL source selection, NLS ambiguity, assertion generation with rectification loops, evaluation beyond coverage metrics, redundancy removal, and long-context handling. For each challenge, the authors present case studies (on designs including a 4-bit RCA, UART, i2c, and GA_68) and propose guidelines in Section III. The paper serves as a perspective/roadmap rather than a full empirical evaluation, and its central claim is that addressing these six challenges can make LLM-based assertion generation more systematic and quality-aware.

Significance. The paper addresses a timely and practically important problem. The identification of vacuity as a quality concern in LLM-generated assertions, the comparison of one-shot vs. rectification-loop methods (Case Study 5), and the structured taxonomy of six challenges are useful contributions to the community. The authors provide a GitHub repository [4] linking to case-study reports, which improves reproducibility. The guidelines in Section III, while unvalidated, offer concrete and falsifiable directions for future framework development.

major comments (3)
  1. [Section II.D, Case Study 6] The paper states: 'The coverage is high primarily due to vacuous assertions as shown in the table below.' This is a causal claim, but the table only demonstrates co-occurrence of vacuity rates (21–36%) and coverage rates (64–92%) across four design/framework combinations. No experiment removes vacuous assertions and re-measures coverage to establish that vacuity is the primary driver of inflated coverage. It is possible that the non-vacuous assertions alone achieve comparable coverage. This matters because Guideline III.D(1) recommends feeding vacuous assertions back to an LLM for refinement, which presupposes that vacuity is the root cause of misleading coverage. The broader Key Takeaway ('coverage metrics are not sufficient') is defensible without the causal claim, but the specific mechanism should either be demonstrated with a removal experiment or the causal language ('primarily due,
  2. [Section III] None of the seven guidelines in Section III have been implemented or tested in this paper. The case studies in Section II demonstrate that problems exist (e.g., signal-name inconsistency, vacuity, low pass rates) but do not validate that the proposed solutions work. For a perspective paper this is partially expected, but the paper should explicitly acknowledge this limitation—ideally in the introduction or conclusion—so that readers understand the guidelines are hypotheses for future work, not validated recommendations. As written, the transition from 'we observed these problems' to 'here are the guidelines' may imply stronger empirical support than exists.
  3. [Section II.D, Case Study 6 table] The vacuity and coverage comparison uses only two designs (i2c, GA_68) and two frameworks (SANGAM, AssertionForge). Whether the observed vacuity rates (21–36%) and the relationship between vacuity and coverage generalize to larger designs or other frameworks is not established. The paper should either expand the evaluation or explicitly state the scope limitation of this case study, particularly since the claim about coverage inflation is presented as a general finding rather than a design-specific observation.
minor comments (6)
  1. [Case Study 4, Comparison Table] The table reports FPV Pass counts (29, 107, 27) but does not report pass rates. Case Study 5 later states the percentages (11.6%, 38.7%, 10.6%), but it would be clearer to include pass rates directly in the Case Study 4 table.
  2. [Case Study 3] The two ambiguity sets are labeled 'Ambiguity Set 1 (AS1)' and 'Ambiguity Set 1 (AS2)' — the second should presumably be 'Ambiguity Set 2 (AS2)'.
  3. [Section II.A] The paper should disclose that three of the reviewed frameworks (ChIRAAG [8], LAAG-RV [9], SANGAM [12]) are co-authored by the present paper's authors. A brief disclosure statement would strengthen the review's credibility.
  4. [Figure 1] The figure caption 'Overall Generalized Steps for LLM-based Assertion Generation' could benefit from labeling which steps correspond to which challenges/guidelines (A–G) to improve cross-referencing between Section II and Section III.
  5. [Section II.E] This section on redundancy and weak assertions is brief and contains no case study or quantitative data, unlike the other challenge subsections. Consider either adding a small illustrative example or noting explicitly that this challenge is motivated by observation rather than measured data.
  6. [References] Several arXiv preprints ([6], [13]) are cited; ensure these are the latest versions. Reference [14] is dated 2026 — verify the publication status.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for a careful and constructive review. The referee raises three major points: (1) the causal language in Case Study 6 regarding vacuity and coverage inflation is not supported by a removal experiment; (2) the guidelines in Section III are unvalidated hypotheses and the paper should explicitly acknowledge this; (3) the scope of Case Study 6 is limited to two designs and two frameworks, and the generalizability of the findings is not established. We agree with all three points and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: Case Study 6 makes a causal claim ('coverage is high primarily due to vacuous assertions') based only on co-occurrence of vacuity and coverage rates, without a removal experiment. The causal language should be demonstrated or softened.

    Authors: The referee is correct. The table in Case Study 6 demonstrates co-occurrence of vacuity rates (21–36%) and coverage rates (64–92%), but we did not perform an experiment in which vacuous assertions are removed and coverage is re-measured. Without that experiment, we cannot substantiate the causal claim that vacuity is the primary driver of inflated coverage. We will revise the manuscript in two ways. First, we will soften the causal language: the sentence 'The coverage is high primarily due to vacuous assertions' will be rewritten as 'The coverage is high, and a significant fraction of the proven assertions are vacuous, suggesting that vacuity may contribute to inflated coverage metrics.' Second, we will add a sentence acknowledging that a removal experiment (removing vacuous assertions and re-measuring coverage) is needed to establish the causal mechanism definitively, and we will note this as future work. We note that the broader Key Takeaway ('coverage metrics are not sufficient') does not depend on the causal claim and remains defensible: the co-occurrence of high vacuity rates and high coverage rates is itself sufficient to motivate the need for vacuity analysis alongside coverage metrics. We will also adjust Guideline III.D(1) to clarify that feeding vacuous assertions back to an LLM for refinement is proposed as a quality-improvement step regardless of whether vacuity is the sole cause of coverage inflation, since vacuous assertions are undesirable in any case. revision: yes

  2. Referee: None of the seven guidelines in Section III have been implemented or tested. The paper should explicitly acknowledge that the guidelines are hypotheses for future work, not validated recommendations.

    Authors: We agree. The paper is a perspective/roadmap, and the guidelines in Section III are proposed directions based on the challenges identified in Section II, not empirically validated solutions. As written, the transition from 'we observed these problems' to 'here are the guidelines' may imply stronger empirical support than exists. We will add an explicit acknowledgment in both the introduction and the conclusion stating that the guidelines are hypotheses for future work and have not been implemented or validated in this paper. Specifically, we will add a sentence at the end of the introduction noting that 'the guidelines proposed in Section III are based on observations from the case studies and the analysis of existing frameworks; they have not been empirically validated in this work and are intended as directions for future research.' We will add a corresponding statement in the conclusion as well. revision: yes

  3. Referee: Case Study 6 uses only two designs (i2c, GA_68) and two frameworks (SANGAM, AssertionForge). The generalizability of the vacuity-coverage relationship to larger designs or other frameworks is not established. The paper should expand the evaluation or state the scope limitation.

    Authors: The referee is correct that the case study is limited to two designs and two frameworks, and the findings should not be presented as general without qualification. Expanding the evaluation to additional designs and frameworks would strengthen the claims, but we are constrained by the availability of open-source frameworks and reproducible case-study artifacts in this emerging area. We will explicitly state the scope limitation of Case Study 6 in the manuscript: the observations are based on two designs (i2c and GA_68) and two frameworks (SANGAM and AssertionForge), and whether the vacuity rates and the relationship between vacuity and coverage generalize to larger designs or other frameworks is not established. We will also reframe the claim about coverage inflation as a design- and framework-specific observation rather than a general finding. If time permits before the camera-ready deadline, we will attempt to add one additional design to broaden the scope, but we commit at minimum to the scope-limitation statement. revision: yes

Circularity Check

0 steps flagged

No significant circularity; the paper is a review/perspective whose guidelines derive from case studies and literature, not from self-referential definitions.

full rationale

This is a review/perspective paper that identifies six challenges in LLM-based assertion generation and proposes guidelines for each. The derivation chain is: case studies (Sections II.A–II.F) → key takeaways → guidelines (Section III). The case studies use external benchmarks (AssertLLM, AssertionForge, SANGAM, JasperGold) and small designs (RCA, UART, i2c, GA_68) to motivate each challenge. While three of the reviewed frameworks (ChIRAAG [8], LAAG-RV [9], SANGAM [12]) are co-authored by the present authors, these are cited as prior work among several others (AssertLLM [10], AssertionForge [11], AssertCoder [13]), not as the sole justification for any claim. The central claim—that these six challenges exist and should be addressed—does not reduce to a self-citation chain: the challenges (specification vs. RTL, NLS ambiguity, rectification loops, coverage insufficiency, redundancy, long-context) are independently observable from the case study data and from the broader literature. The guidelines in Section III are forward-looking recommendations, not claimed as validated results. No equation or definition in the paper is circular with respect to its inputs. The causal claim in Case Study 6 ('coverage is high primarily due to vacuous assertions') is a correctness concern (correlation vs. causation), not a circularity concern—it does not reduce to its inputs by construction. The paper does not fit a parameter to data and then rename the fit as a prediction, nor does it define a quantity in terms of what it claims to derive. The self-citations are normal scholarly practice for a review by active researchers in the area and are not load-bearing for the central thesis in a way that would make the argument circular.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

The paper is a review/perspective with no new methods, parameters, or entities. The axioms are domain assumptions about LLM behavior in assertion generation, supported by limited case studies but generalized to guidelines. The KG-based representation recommendation is an ad-hoc guideline not independently validated in this paper.

axioms (4)
  • domain assumption LLM-generated assertions from RTL may encode implementation bugs rather than specification intent
    Stated in Section II.A: 'generating assertions directly from RTL or code comments may produce incomplete or misleading properties.' This is a domain assumption about LLM behavior, supported by Case Study 1 but assumed as general.
  • domain assumption Coverage metrics (formal coverage, branch coverage, toggle coverage) are insufficient to evaluate assertion quality
    Stated in Section II.D and Case Study 6. The paper assumes that vacuity analysis and COI-based analysis are needed beyond coverage metrics, supported by two data points (i2c, GA_68) but generalized.
  • domain assumption Signal-name inconsistency between specifications and RTL is a primary cause of vacuous proofs in LLM-generated assertions
    Stated in Section II.D: 'signal inconsistency between the RTL implementation and the generated assertions can lead to vacuous proofs.' Case Study 6 provides evidence but the causal link is assumed.
  • ad hoc to paper Knowledge-graph-based specification representation reduces ambiguity in NLS for LLM-based assertion generation
    Proposed in Section III.C as a guideline. The paper does not provide experimental evidence that KG-based representation outperforms other structured forms; it is a recommendation based on AssertionForge's approach.

pith-pipeline@v1.1.0-glm · 12246 in / 2563 out tokens · 403066 ms · 2026-07-09T10:30:53.987403+00:00 · methodology

0 comments
read the original abstract

Assertion-based Verification (ABV) plays a critical role in the Design Verification (DV) process. However, ABV requires substantial manual effort in generating assertion from specification by verification engineers, making it a time-consuming stage in the chip design flow. With the recent development of Large Language Models (LLMs), researchers have started exploring their use as an assistance in the ABV process, particularly for generating SystemVerilog Assertions (SVAs) from design specification. In this paper, we provide an overview of recent works, highlighting the different methods used to generate SVAs. In particular, we investigate LLM-based SVA generation and ask a central question: How can LLM-based assertion generation be made systematic and quality-aware? While addressing this key question, we provide Key Takeaways at the end of each challenge, summarizing the important methodological insights, and also provide guidelines and directions in solving those challenges that can help generate a high-quality set of assertions using LLMs.

Figures

Figures reproduced from arXiv: 2607.07444 by Bhabesh Mali, Chandan Karfa.

Figure 1
Figure 1. Figure 1: Overall Generalized Steps for LLM-based Assertion Generation [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages · 2 internal anchors

  1. [1]

    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,” inDATE 2010. IEEE, 2010, pp. 626–629

    work page 2010

  2. [2]

    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,” inNinth ACM/IEEE MEMOCODE. IEEE, 2011, pp. 191–200

    work page 2011

  3. [3]

    Attention is all you need,

    A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin, “Attention is all you need,”NeurIPS, vol. 30, 2017

    work page 2017

  4. [4]

    LLM-Based Assertion Generation: Lessons and Future Directions,

    B. Mali, “LLM-Based Assertion Generation: Lessons and Future Directions,” https://github.com/BhabeshMali/LLM-Based-Assertion- Generation-Lessons-and-Future-Directions-, 2026, gitHub repository

    work page 2026

  5. [5]

    2024 wilson research group ic/asic functional verification trend report,

    H. D. Foster, “2024 wilson research group ic/asic functional verification trend report,” Siemens Digital Industries Software, White Paper, 2024, online; accessed 5 March 2026. [Online]. Available: https://resources.sw.siemens.com/en-US/white-paper-2024- wilson-research-group-ic-asic-functional-verification-trend-report/

    work page 2024

  6. [6]

    Using LLMs to Facilitate Formal Verification of RTL

    M. Orenes-Vera, M. Martonosi, and D. Wentzlaff, “Using llms to facilitate formal verification of rtl,” 2023. [Online]. Available: https://arxiv.org/abs/2309.09437

    work page internal anchor Pith review Pith/arXiv arXiv 2023

  7. [7]

    (security) assertions by large language models,

    R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “(security) assertions by large language models,”IEEE TIFS, 2024

    work page 2024

  8. [8]

    Chiraag: Chatgpt informed rapid and automated assertion generation,

    B. Mali, K. Maddala, V . Gupta, S. Reddy, C. Karfa, and R. Karri, “Chiraag: Chatgpt informed rapid and automated assertion generation,” in2024 IEEE ISVLSI, 2024, pp. 680–683

    work page 2024

  9. [9]

    Laag-rv: Llm assisted assertion generation for rtl design verification,

    K. Maddala, B. Mali, and C. Karfa, “Laag-rv: Llm assisted assertion generation for rtl design verification,” in2024 IEEE ITC India, pp. 1–6

    work page

  10. [10]

    Assertllm: Generating hardware verification assertions from design specifications via multi-llms,

    Z. Yan, W. Fang, M. Li, M. Li, S. Liu, Z. Xie, and H. Zhang, “Assertllm: Generating hardware verification assertions from design specifications via multi-llms,” inProceedings of the 30th Asia and South Pacific Design Automation Conference, 2025, pp. 614–621

    work page 2025

  11. [11]

    Assertionforge: Enhancing formal verification assertion generation with structured representation of specifications and rtl,

    Y . Bai, G. B. Hamad, S. Suhaib, and H. Ren, “Assertionforge: Enhancing formal verification assertion generation with structured representation of specifications and rtl,” in2025 IEEE ICLAD, pp. 85–92

    work page

  12. [12]

    Sangam: Systemverilog assertion generation via monte carlo tree self-refine,

    A. Gupta, B. Mali, and C. Karfa, “Sangam: Systemverilog assertion generation via monte carlo tree self-refine,” in2025 IEEE ICLAD

    work page

  13. [13]

    AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction

    E. Tian, Y . Ci, Q. Yang, Y . Li, and Z. Lyu, “Assertcoder: Llm-based assertion generation via multimodal specification extraction,”arXiv preprint arXiv:2507.10338, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  14. [14]

    Fixme: Towards end-to-end bench- marking of llm-aided design verification,

    G.-W. Wan, S. Wong, S. Su, C. Niu, N. Wang, X. Wan, Q. Chen, M. Xing, J. Zhang, J. Yeet al., “Fixme: Towards end-to-end bench- marking of llm-aided design verification,” inAAAI, vol. 40, no. 2, 2026, pp. 1087–1095

    work page 2026

  15. [15]

    Make your llm fully utilize the context,

    S. An, Z. Ma, Z. Lin, N. Zheng, J.-G. Lou, and W. Chen, “Make your llm fully utilize the context,”Advances in Neural Information Processing Systems, vol. 37, pp. 62 160–62 188, 2024

    work page 2024

  16. [16]

    Dasgupta,A Roadmap for Formal Property Verification

    P. Dasgupta,A Roadmap for Formal Property Verification. Berlin, Heidelberg: Springer-Verlag, 2006

    work page 2006

  17. [17]

    GraphRAG Documentation,

    Microsoft, “GraphRAG Documentation,” https://microsoft.github.io/graphrag/, 2025, online documentation

    work page 2025

  18. [18]

    LlamaParse Platform Quickstart,

    LlamaIndex, “LlamaParse Platform Quickstart,” https://developers.llamaindex.ai/llamaparse/, 2026, developer documentation

    work page 2026