Pith. sign in

REVIEW 5 major objections 6 minor 24 references

LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation

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

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

Pith's one-line read LASA claims an automated LLM pipeline with retrieval augmentation, vacuity filtering, and coverage-driven refinement can generate non-vacuous security properties for bus-based SoCs at roughly 88% average formal coverage and detect five…

desk verdict A real engineering integration with five genuine bug catches on Hack@DAC'24, but the headline non-vacuity claim rests on an LLM prompt rather than a formal check. read the letter →

arxiv 2506.17865 v1 pith:EMPUBBCP submitted 2025-06-22 cs.CR cs.ET

Dinesh Reddy Ankireddy , Sudipta Paria , Aritra Dasgupta , Sandip Ray , Swarup Bhunia This is my paper
classification cs.CRcs.ET
keywords SoCsecurityverificationSystemVerilogassertionsformalpropertyLLM-aidedvacuitycheckingretrieval-augmentedgenerationcoverageanalysishardwarebugdetection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper is trying to establish that an automated pipeline can replace much of the manual labor in SoC security verification: a large language model, supplied with design specifications and documentation via retrieval-augmented generation, produces security properties and SystemVerilog assertions that are non-vacuous, achieve high formal coverage, and can find real hardware bugs. A vacuous property is one that passes only because its triggering condition never occurs, so it verifies nothing. The reported average coverage is about 88% across eight IP blocks from two open-source SoCs, and the framework is credited with finding five bugs in a buggy OpenTitan design from the Hack@DAC'24 competition. The payoff, if true, is a verification workflow where property writing, vacuity filtering, coverage measurement, and prompt refinement are automated, with a commercial model checker used to prove or refute the final assertions.

What carries the argument

The central mechanism is the vacuity-checked generation loop: a set of nine vacuity theorems from temporal model checking is encoded as k-shot rules in prompts, and the LLM is asked to filter its own generated properties so that only non-vacuous ones proceed. Non-vacuous properties are then converted to SystemVerilog assertions, checked by a commercial formal-property-verification tool for proofs and counterexamples, and scored with checker, stimuli, and formal coverage metrics. When coverage falls below the configured threshold, the loop feeds coverage-report context back into the prompts to generate additional assertions, repeating until the threshold is met.

What would settle it

Take the 41 AES-192 properties that LASA labels non-vacuous and, for each, replace one subformula with true and then with false, model-checking both versions against the same design; if any property has a subformula for which both checks pass (meaning the property holds regardless of that subformula), that property is vacuous, and a non-trivial number of such findings would refute the central guarantee.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that a structured pipeline—JSON spec templates plus RAG-extracted documentation, k-shot prompting with nine vacuity theorems, SVA translation with re-prompting for syntax errors, and formal-property-verification coverage analysis with an 80% threshold and iterative prompt refinement—produces security properties that are mostly non-vacuous, provable, and coverage-rich. The paper reports per IP that most generated properties survive vacuity filtering and that checker and formal coverage values exceed the threshold across AES-192, DES3, GPS, FIR, IIR, i2c, adc_ctrl, and kmac. It further reports five bug detections in the Hack@DAC'24 OpenTitan SoC, each tied to a specific SVA that exposes a security-relevant violation. The author would state it as: LASA demonstrates that LLM-based security property generation can be made non-vacuous and coverage-aware, and that the resulting assertions are strong enough to catch real bugs.

Load-bearing premise

The load-bearing premise is that a large language model, prompted with nine textual vacuity rules and no formal model checker, correctly decides which generated properties are vacuous; if that judgment is often wrong, the 'non-vacuous' guarantee and the coverage numbers built on it no longer mean what the paper says.

Editorial extensions

If this is right

  • If LASA is correct, automated security property generation can reach roughly 88% average formal coverage while filtering out vacuous assertions, reducing the manual effort in assertion-based SoC verification.
  • The iterative refinement loop shows that coverage reports can be used as feedback to an LLM to generate additional, relevant assertions rather than requiring a human to rewrite them.
  • The five OpenTitan bug detections imply that LLM-generated assertions can act as bug hunters, not just coverage fillers, when prompts include threat models, secure assets, and micro-architectural events.
  • The modular treatment of IPs and submodules points to a scalable way to apply LLM-based verification to large SoCs without exceeding token limits.
  • Filtering properties by vacuity before running expensive model checking can reduce wasted formal-verification effort on trivial assertions.

Reading between the lines

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

  • Inference: A direct testable extension is to run the same generated 'non-vacuous' properties through an independent formal vacuity checker—mutating subformulas to true and false and model-checking both versions—to measure how often the LLM's vacuity judgment agrees with the theorems.
  • Inference: High coverage of generated assertions does not by itself establish security, because coverage measures exercised logic rather than the absence of all attacks; a stronger claim would need additional security-specific metrics.
  • Inference: The same RAG-plus-vacuity-plus-coverage loop could plausibly transfer to other interconnect fabrics and abstraction levels, such as Network-on-Chip designs, if the prompt templates and vacuity rules are adapted accordingly.
  • Inference: The five detected bugs are a small sample; a more general statement about bug-detection power would require injecting or comparing against a larger set of known bugs across multiple designs.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 6 minor

Summary. The paper presents LASA, an LLM-based framework that generates security properties and SystemVerilog Assertions (SVAs) for bus-based SoCs. The pipeline combines RAG-based prompt construction, k-shot learning, an LLM-mediated vacuity check based on nine theorems from the temporal-logic literature, SVA generation, and FPV with Cadence JasperGold for coverage analysis; if coverage falls below a configured threshold (set to 80%), LASA iteratively refines the prompts and generates additional assertions. The authors evaluate on IPs from the CEP and OpenTitan SoCs, reporting coverage values that they summarize as an average of about 88%, and they claim detection of five bugs in the buggy OpenTitan benchmark from Hack@DAC'24.

Significance. If the claims hold, LASA would be a valuable step toward automating security-property generation, combining RAG, k-shot prompting, FPV coverage feedback, and bug detection in a single framework. The external ground truth from the Hack@DAC'24 buggy OpenTitan is a genuine strength, and the integration with JasperGold gives the work a concrete engineering orientation. However, the central evidence is weakened in three ways: the vacuity check—the feature that distinguishes LASA from prior LLM-based generators—is implemented as an LLM prompt rather than a formal model-checking step; the headline coverage number is not directly supported by the tables and is confounded by the fact that coverage is the termination criterion for iterative refinement; and no quantitative baseline comparison to prior LLM-based assertion generators is provided. The framework is plausible and the bug-detection results are promising, but the current evidence is suggestive rather than conclusive.

major comments (5)
  1. [Section III-B, Appendix Prompt 3] The central guarantee of generating non-vacuous properties is not formally established. The paper says LASA 'incorporates vacuous rules checking' and borrows the nine theorems from the literature, but no algorithm or tool invocation is described that checks Theorem 1's condition, M ⊨ φ[ψ←true] iff M ⊨ φ[ψ←false], on the design model. Instead, Appendix Prompt 3 asks the LLM to classify each generated property as vacuous or non-vacuous based on a textual prompt. An LLM's classification cannot verify the equivalence of mutated formulas, so the survival of a property through this stage, and hence the property set used for coverage computation, depends on an unvalidated heuristic. In addition, Section IV-C states that LASA discards 'all non-vacuous properties that violate at least one of nine theorems,' which is the opposite of the intended behavior and suggests a possible inversion of the vacuity definition. The authors should either replace the LLM-based vacuity filter with a formal model-checking step that implements Theorem 1 or, at minimum, validate the LLM's vacuity labels against formal ground truth on a representative sample of generated properties.
  2. [Section IV-E, Table III, Abstract] The claimed 'average of ~88%' coverage is not supported by the data in Table III. The Average row is left blank, and computing the mean of the Formal Coverage 'Proof Core' column over the eight IPs gives approximately 83.8% (the Checker Coverage 'Proof Core' mean is similarly about 83.3%). None of the reported columns averages to 88%, so the paper should state which metric corresponds to the headline number and fill in the average row. Furthermore, because Section III-E defines iterative refinement as continuing until a pre-defined coverage threshold (80%) is met, the reported coverage values are by construction post-threshold values; using them as the primary evidence of verification completeness is self-referential. The authors should report coverage before iterative refinement or compare against a baseline property set to separate the effect of refinement from the effect of threshold targeting.
  3. [Section IV, Table I] The experimental evaluation lacks any quantitative comparison to prior LLM-based property/assertion generation methods such as AssertLLM, LASP, or Kande et al., even though Table I claims qualitative advantages over these approaches. Without running at least one baseline method on the same IPs, or comparing on a common benchmark with the same coverage metrics, it is unclear whether LASA's coverage and non-vacuity results represent an actual improvement. This is particularly important because the coverage metric is the main reported success measure, and the baseline methods may produce different numbers of assertions or different coverage profiles on the same designs.
  4. [Section IV-G, Table IV] The bug detection evaluation is under-specified. The paper says LASA detected five bugs in the Hack@DAC'24 buggy OpenTitan, but it does not describe the concrete workflow that produced the SVAs in Table IV, how many assertions were generated before these five were identified, how many false positives occurred, or whether these properties were obtained without manual intervention. Two of the listed properties (bugs 3 and 5) are unconditional assertions with no antecedent, so it is unclear how they relate to the stated bug conditions and whether they pass the paper's own vacuity filter. The table also contains typographical errors (e.g., 'Line: 76-66' for bug 5) that complicate assessment. Without a clear methodology and false-positive count, the bug-detection claim cannot be independently verified.
  5. [Section IV-C, Table II] The column '#correct' in Table II is not rigorously defined. The text says it denotes properties that are 'proven to be relevant and semantically correct,' but no gold standard or decision procedure is described. If correctness is judged by JasperGold proofs, then failed-but-meaningful assertions, which are important for bug detection, would be counted as incorrect; if it is judged by human experts, the evaluation is subjective and should be documented with an inter-rater or audit protocol. The paper should specify how the correctness label is assigned, since the reported property-generation quality depends on this definition.
minor comments (6)
  1. [Section IV-C, Listings 2 and 3] The listing cross-references are inconsistent: the text says 'Listing 3 demonstrates an example vacuous property' but the displayed code is labeled Listing 2, and later the text says 'Listing 3 illustrates a counterexample' while Listing 3 is actually a property declaration. Please renumber the listings or fix the in-text references.
  2. [Appendix B, Table V] The GPS block of Table V contains repeated AES-192 rows: AES_192_top, Expand_key_type_A, Expand_key_type_B, Expand_key_type_C, Expand_key_type_D, and final_round appear both under AES-192 and again under GPS. This appears to be a copy-paste error and should be corrected.
  3. [Table III] The Average row is left empty; please fill it with the computed means for each column and specify which metric corresponds to the '~88%' claim in the abstract and conclusion.
  4. [Section II-B] Theorems 4–9 use the terms 'linearly witnessable' and 'linearly counterable' without definitions, and these theorems are not used elsewhere in the paper. Either provide brief definitions or move these complexity results to a reference, since the current presentation may confuse readers unfamiliar with the vacuity literature.
  5. [Figure 2] The y-axis of Figure 2 is not labeled, and it is unclear whether the plotted values are percentages of generated properties that are proved/failed, or absolute counts, or normalized scores. Please add axis labels and explain the metric in the caption.
  6. [Appendix Prompt 3] The sentence 'A property must fail at least one vacuity condition among the 9 theorems to be non-vacuous' is logically ambiguous; a property is non-vacuous when no subformula is irrelevant, which is the negation of the vacuity condition, not a 'failure' of a theorem. Rewording this prompt is necessary for conceptual clarity, especially since the vacuity-check stage is a key contribution.

Circularity Check

1 steps flagged · score 4.0 of 10

Coverage is both the optimization target and the reported success metric, so the ~88% average is partly forced by the 80% stopping threshold; the vacuity guarantee rests on an unverified LLM label, but Hack@DAC bug detection provides external grounding.

  1. other [Section III-E and Section IV-E]
    "LASA employs iterative refinement that enhances the existing prompts to improve the coverage by generating additional properties followed by SVAs until the pre-defined coverage threshold (%) is met. ... LASA follows a configurable coverage threshold (set to 80% for our experiments), representing the minimum coverage required for the verification to be considered acceptable. If coverage falls below this threshold, LASA incoprates a feedback loop to generate additional relevant SVAs to improve the coverage."

    The coverage values reported in Table III are the output of a loop whose stopping condition is the same coverage value. Because refinement terminates only after coverage meets or exceeds the 80% threshold, the reported average of ~88% is a direct consequence of the stopping rule rather than an independent measure of the quality or completeness of the generated security properties. The paper then uses these threshold-satisfying coverage numbers as evidence of 'comprehensive verification,' so the evaluation metric is also the optimization target. The Hack@DAC bug detections are external and prevent the work from being fully circular, but the headline coverage claim is partly manufactured by the algorithm's own criterion.

full rationale

No formal derivation in the paper reduces an equation or a fitted parameter to its own input, and the central vacuity theorems are cited from external literature (Kupferman and Vardi; Beer et al.), not from the authors' own prior work. The most significant circularity concern is the coverage evaluation: the framework iteratively adds assertions until coverage reaches a predefined threshold, and then reports high coverage as evidence of effectiveness. This is self-referential in that the reported metric is the quantity being optimized, making the ~88% average largely an artifact of the 80% stopping criterion. The vacuity-checking stage, implemented only as an LLM prompt (Appendix Prompt 3), is a validity and correctness risk rather than a circular step: the paper does not formally verify the model-equivalence condition of Theorem 1, so the 'non-vacuous' label is an unverified LLM classification. The bug-detection results on the Hack@DAC'24 OpenTitan benchmark provide independent, externally defined evidence that LASA can find real flaws, which justifies not assigning a higher circularity score. Overall, the coverage claim is partially circular, but the work retains independent content through its bug findings, so a moderate score of 4 is appropriate.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The framework has no new physical or formal entities. It imports standard vacuity theorems from the literature, assumes the LLM can apply them correctly, assumes coverage metrics reflect security completeness, and assumes the input specifications are accurate. No numeric free parameters appear beyond the hand-set 80% coverage threshold and the unspecified k-shot count.

free parameters (2)
  • coverage threshold = 80%
    Hand-chosen stopping criterion in LASA's iterative refinement (Sections III-E and IV-E). The reported coverage values are partly a consequence of this threshold, and no sensitivity analysis is given.
  • k in k-shot learning = not specified
    The number of example assertions used in prompts is not reported, which is a reproducibility gap and affects the quality of generated properties.
assumptions (4)
  • standard math The nine vacuity theorems from Kupferman and Vardi [16] and Beer et al. [17] are valid and applicable to the generated LTL/CTL properties.
    Borrowed from cited literature in Section II-B and used as the basis for vacuity filtering.
  • ad hoc to paper An LLM can correctly apply the nine vacuity rules to generated properties when prompted.
    LASA has no formal vacuity checker; the framework prompts the LLM to classify each property as vacuous or not (Section III-B, Appendix Prompt 3), without accuracy evaluation.
  • domain assumption JasperGold coverage metrics (stimuli, checker, formal) are a meaningful proxy for security verification completeness.
    The paper equates high coverage with 'comprehensive verification' in Section IV-E without a ground-truth security benchmark.
  • domain assumption The design specifications, documentation, and RTL provided to LASA are accurate and sufficient for property generation.
    Prompt generation relies on JSON spec files and RAG-extracted documentation (Section III-A); incorrect specs would produce meaningless properties.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation." pith.science (2026). https://pith.science/paper/EMPUBBCP

@misc{pith2026250617865,
  author       = {Pith},
  title        = {Pith review of: LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EMPUBBCP}},
  note         = {Machine review of arXiv:2506.17865}
}
read the original abstract

Ensuring the security of modern System-on-Chip (SoC) designs poses significant challenges due to increasing complexity and distributed assets across the intellectual property (IP) blocks. Formal property verification (FPV) provides the capability to model and validate design behaviors through security properties with model checkers; however, current practices require significant manual efforts to create such properties, making them time-consuming, costly, and error-prone. The emergence of Large Language Models (LLMs) has showcased remarkable proficiency across diverse domains, including HDL code generation and verification tasks. Current LLM-based techniques often produce vacuous assertions and lack efficient prompt generation, comprehensive verification, and bug detection. This paper presents LASA, a novel framework that leverages LLMs and retrieval-augmented generation (RAG) to produce non-vacuous security properties and SystemVerilog Assertions (SVA) from design specifications and related documentation for bus-based SoC designs. LASA integrates commercial EDA tool for FPV to generate coverage metrics and iteratively refines prompts through a feedback loop to enhance coverage. The effectiveness of LASA is validated through various open-source SoC designs, demonstrating high coverage values with an average of ~88\%, denoting comprehensive verification through efficient generation of security properties and SVAs. LASA also demonstrates bug detection capabilities, identifying five unique bugs in the buggy OpenTitan SoC from Hack@DAC'24 competition.

Figures

Figures reproduced from arXiv: 2506.17865 by the authors.

Figure 1
Figure 1. Major stages in the proposed LASA framework. B. Security Property Generation The proposed framework leverages pre-trained LLMs to generate relevant security properties for the SoC design under [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Comparing LLMs in terms of generating properties. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Number of ‘Proved’ and ‘Failed’ Properties Generated [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Timing diagram depicting the counterexample (CEX). [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Improvement on coverage values for different IPs [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

24 extracted references · 21 canonical work pages

  1. [1]

    Bhunia and M

    S. Bhunia and M. Tehranipoor, Hardware Security: A Hands-on Learn- ing Approach, 1st ed. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2018

    work page 2018

  2. [2]

    A survey on assertion- based hardware verification,

    H. Witharana, Y . Lyu, S. Charles, and P. Mishra, “A survey on assertion- based hardware verification,” ACM Comput. Surv., vol. 54, no. 11s, Sep. 2022

    work page 2022

  3. [3]

    Synfuzz: Leveraging fuzzing of netlist to detect synthesis bugs,

    R. Saravanan, S. Paria, A. Dasgupta, V . N. Patnala, S. Bhunia, and S. M. P. D, “Synfuzz: Leveraging fuzzing of netlist to detect synthesis bugs,” 2025. [Online]. Available: https://arxiv.org/abs/2504.18812

    arXiv 2025

  4. [4]

    Hypfuzz: formal-assisted processor fuzzing,

    C. Chen, R. Kande, N. Nguyen, F. Andersen, A. Tyagi, A.-R. Sadeghi, and J. Rajendran, “Hypfuzz: formal-assisted processor fuzzing,” in Proceedings of the 32nd USENIX Conference on Security Symposium , ser. SEC ’23. USA: USENIX Association, 2023

    work page 2023

  5. [5]

    Navigating soc security landscape on llm-guided paths,

    S. Paria, A. Dasgupta, and S. Bhunia, “Navigating soc security landscape on llm-guided paths,” in Proceedings of the Great Lakes Symposium on VLSI 2024, ser. GLSVLSI ’24. New York, NY , USA: Association for Computing Machinery, 2024, p. 252–257

    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

    work page 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 Transactions on Information Forensics and Security , pp. 1–1, 2024

    work page 2024

  8. [8]

    SPELL: An End-to-End Tool Flow for LLM-Guided Secure SoC Design for Embedded Systems,

    S. Paria, A. Dasgupta, and S. Bhunia, “SPELL: An End-to-End Tool Flow for LLM-Guided Secure SoC Design for Embedded Systems,” IEEE Embedded Systems Letters , vol. 16, no. 4, pp. 365–368, 2024

    work page 2024

Show all 24 references
  1. [9]

    As- sertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs,

    W. Fang, M. Li, M. Li, Z. Yan, S. Liu, H. Zhang, and Z. Xie, “As- sertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs,” 2024

    2024

  2. [10]

    Unlocking Hardware Security Assurance: The Potential of LLMs,

    X. Meng, A. Srivastava, A. Arunachalam, A. Ray, P. H. Silva, R. Psiakis, Y . Makris, and K. Basu, “Unlocking Hardware Security Assurance: The Potential of LLMs,” 2023

    2023

  3. [11]

    LASP: LLM Assisted Security Property Generation for SoC Verifica- tion,

    A. Ayalasomayajula, R. Guo, J. Zhou, S. K. Saha, and F. Farahmandi, “LASP: LLM Assisted Security Property Generation for SoC Verifica- tion,” in 2024 ACM/IEEE 6th Symposium on Machine Learning for CAD (MLCAD), 2024, pp. 1–7

    2024

  4. [12]

    Examining Zero-Shot Vulnerability Repair with Large Language Models,

    H. Pearce, B. Tan, B. Ahmad, R. Karri, and B. Dolan-Gavitt, “Examining Zero-Shot Vulnerability Repair with Large Language Models,” in 2023 IEEE Symposium on Security and Privacy (SP) , 2023, pp. 2339–2356

    2023

  5. [13]

    Fixing Hardware Security Bugs with Large Language Models,

    B. Ahmad, S. Thakur, B. Tan, R. Karri, and H. Pearce, “Fixing Hardware Security Bugs with Large Language Models,” 2023

    2023

  6. [14]

    DIV AS: An LLM-based End-to- End Framework for SoC Security Analysis and Policy-based Protection,

    S. Paria, A. Dasgupta, and S. Bhunia, “DIV AS: An LLM-based End-to- End Framework for SoC Security Analysis and Policy-based Protection,” 2023

    2023

  7. [15]

    DiSPEL: A Framework for SoC Security Policy Synthesis and Distributed Enforcement,

    S. Paria, A. Dasgupta, and S. Bhunia, “DiSPEL: A Framework for SoC Security Policy Synthesis and Distributed Enforcement,” in 2024 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 2024, pp. 271–281

    2024

  8. [16]

    Vacuity detection in temporal model checking,

    O. Kupferman and M. Y . Vardi, “Vacuity detection in temporal model checking,” in Correct Hardware Design and Verification Methods , L. Pierre and T. Kropf, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 82–98

    1999

  9. [17]

    Efficient detection of vacuity in actl formulas,

    I. Beer, S. Ben-David, C. Eisner, and Y . Rodeh, “Efficient detection of vacuity in actl formulas,” in Computer Aided Verification, O. Grumberg, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997, pp. 279–290

    1997

  10. [18]

    Clip: A structural approach to cut points matching for logic equivalence checking,

    D. R. Ankireddy, S. Paria, A. Dasgupta, S. Ray, and S. Bhunia, “Clip: A structural approach to cut points matching for logic equivalence checking,” in 2025 IEEE 43rd VLSI Test Symposium (VTS) , 2025, pp. 1–7

    2025

  11. [19]

    ChipNeMo: Domain-Adapted LLMs for Chip Design,

    M. Liu et al. , “ChipNeMo: Domain-Adapted LLMs for Chip Design,” 2024

    2024

  12. [20]

    LLM-guided Formal Verification Coupled with Mutation Testing,

    M. Hassan, S. Ahmadi-Pour, K. Qayyum, C. K. Jha, and R. Drechsler, “LLM-guided Formal Verification Coupled with Mutation Testing,” 2024

    2024

  13. [21]

    LLM for SoC Security: A Paradigm Shift,

    D. Saha, S. Tarek, K. Yahyaei, S. K. Saha, J. Zhou, M. Tehranipoor, and F. Farahmandi, “LLM for SoC Security: A Paradigm Shift,” 2023

    2023

  14. [22]

    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,” 2024. [Online]. Available: https://arxiv.org/abs/2409.15281

    2024 arXiv

  15. [23]

    FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware,

    M. Kang, M. Liu, G. B. Hamad, S. Suhaib, and H. Ren, “FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware,” 2024. [Online]. Available: https://arxiv.org/abs/2410.23299

    2024 arXiv

  16. [24]

    Towards automated verification of ip and cots: Leveraging llms in pre- and post-silicon stages,

    S. Paria, A. Dasgupta, and S. Bhunia, “Towards automated verification of ip and cots: Leveraging llms in pre- and post-silicon stages,” in 2025 IEEE 43rd VLSI Test Symposium (VTS) , 2025, pp. 1–5. APPENDIX A. Example Prompts Prompt 1 : Initial Prompt You are an expert in Forma...

    2025

Pith tools

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