Pith. sign in

REVIEW 5 major objections 6 minor 1 cited by

Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA

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

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

Pith's one-line read A customized retrieval pipeline and step-by-step fine-tuning data raise the number of functionally correct SystemVerilog Assertions an LLM generates by roughly 59 percent.

desk verdict A genuinely engineered NL2SVA pipeline with a real FPV-checked benchmark, but the fine-tuning gains rest on an unverified no-overlap assumption between the 4,070 training SVAs and 229 test SVAs. read the letter →

arxiv 2506.21569 v1 pith:4BPRN6BC submitted 2025-06-12 cs.CL cs.AI

Weihua Xiao , Derek Ekberg , Siddharth Garg , Ramesh Karri This is my paper
classification cs.CLcs.AI
keywords SystemVerilogAssertionsNL2SVAretrieval-augmentedgenerationHybridRetrievalprompt-guidedexplanationsfine-tuninghardwareverificationformalproperty
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 translating natural-language hardware properties into SystemVerilog Assertions (NL2SVA) is an engineering problem that custom retrieval and training data can mostly solve, not a limitation of current LLMs. The authors show that a retrieval pipeline built around the structure of SVAs—code-centric chunking, a hybrid semantic-plus-operator retrieval, and an operator rechecking step—lifts the number of functionally matched assertions by 58.42% over a strong general-purpose LLM. They also show that a lightweight 7B model fine-tuned on explanations that walk through the layer-by-layer construction of an SVA matches or beats much larger models, with a 59.05% gain over its base version when retrieval is added. Because SVAs are a standard but labor-intensive part of hardware verification, the payoff is that LLMs could take over much of the manual assertion-writing work. The paper backs these claims with the largest NL2SVA evaluation dataset to date: 40 Verilog designs and 229 formally verified SVAs scored by a formal verification tool for both syntax and functional equivalence.

What carries the argument

The load-bearing machinery is a pair of task-specific customizations. On the retrieval side, dynamic splitting constructs a code database by grouping each SVA code example with the paragraph before and after it, preserving the semantic context that fixed-size chunking destroys; HybridRetrieval then runs two parallel paths, a global semantic search over the whole specification and a keyword-guided search that first decomposes the specification into signal-level operations, maps them to one of the ten SVA operators, and retrieves chunks explaining those operators. A final operator-based rechecking pass retrieves explanations for the operators the LLM actually used and asks the LLM to correct timing and logic mismatches. On the training side, the synthetic fine-tuning dataset replaces plain (SVA, explanation) pairs with prompt-guided explanations that reconstruct each assertion recursively through the Boolean, sequence, property, and verification layers, teaching a lightweight model to build the assertion the same way an engineer would.

What would settle it

Take an independent set of natural-language property descriptions written by engineers outside the author team from real design specifications, apply the fine-tuned 7B model with HybridRetrieval under the same prompting and evaluation protocol, and count functionality-matched assertions with formal verification. If the roughly 59% improvement over the base model does not reproduce—or if retrieval adds little on those outside descriptions—the framework's generality is not established.

Watch

Extended reading notes

Core claim

The paper claims that NL2SVA accuracy is limited not mainly by base model capability but by how SVA-relevant context is retrieved and how the task is taught. A generic RAG that chunks textbooks by fixed size and retrieves only by global semantic similarity fails to deliver useful operator knowledge; a RAG tailored to SVA structure—dynamic splitting, HybridRetrieval, and SVA operator-based rechecking—raises the number of functionally matched assertions by 58.42% over a strong general-purpose LLM and by 34.5% over a code-specialized LLM. For lightweight models, fine-tuning on prompt-guided explanations that reconstruct each SVA layer by layer raises functionality match by 40.95% over the base model, and adding HybridRetrieval brings the total gain to 59.05%. These results are measured on the largest evaluation dataset built for the task, 40 Verilog designs and 229 formally verified SVAs, using a formal verification tool for both syntax correctness and functional equivalence.

Load-bearing premise

The evaluation dataset's natural-language property descriptions were hand-written by the authors and may share stylistic patterns with the synthetic fine-tuning explanations, so the measured gains could overstate performance on independent, real-world specifications.

Editorial extensions

If this is right

  • If the central claim is right, hardware teams can use the customized RAG pipeline with closed large models to get functionally correct SVAs without a domain expert writing assertions by hand.
  • A lightweight model fine-tuned on construction traces plus HybridRetrieval can approach or exceed the assertion quality of much larger models, lowering the compute cost for NL2SVA automation.
  • The operator-based rechecking step mainly improves syntax correctness on its own, so its value is as a safety net; the functional gains come from retrieval and prompt-guided training.
  • The new evaluation dataset gives the NL2SVA community a common ground of 229 formally verified SVAs with syntax and functionality metrics, enabling direct comparison of future methods.

Reading between the lines

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

  • Because the evaluation properties were hand-written by the authors and the training explanations were synthesized from the same operator tables, the 58-59 percent figures may partly reflect stylistic overlap; a reader should treat them as upper-bound estimates until independent test data exist.
  • The same recipe—code-centric chunking, operator-aware retrieval, and construction-trace fine-tuning—could plausibly transfer to other structured formal languages such as PSL or temporal logic formulas, where hierarchical construction from natural-language descriptions is the bottleneck.
  • RAG gains were small for a very strong base model, so retrieval value likely depends inversely on base-model capability; the framework is probably most useful for mid-size and lightweight models.
  • The prompt-guided explanation format could be ablated step by step to identify which construction stage contributes the most, which would guide cheaper generation of fine-tuning data.
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 manuscript proposes Hybrid-NL2SVA, a pipeline that combines a customized retrieval-augmented generation (RAG) framework with a synthetic fine-tuning dataset for translating natural-language hardware property descriptions into SystemVerilog Assertions (NL2SVA). The RAG framework introduces dynamic splitting for database construction, HybridRetrieval that combines global semantic retrieval with keyword-guided operator retrieval, and an SVA operator-based rechecking step. The fine-tuning dataset contains 4,070 SVA/explanation pairs with prompt-guided, layer-by-layer construction traces generated by OpenAI o4-mini. The authors also construct an evaluation dataset of 40 Verilog designs and 229 formally verified SVAs with manually written natural-language property descriptions. Experiments on GPT-4o-mini, CodeX, DeepSeek-V3, and Qwen2.5-Coder-7B-Instruct variants report syntax correctness (SC) and functionality match (FM) measured with Cadence JasperGold. The headline results are a 58.42% FM improvement from the customized RAG framework over GPT-4o-mini and a 59.05% FM improvement from prompt-fine-tuned Qwen combined with HybridRetrieval over the base Qwen model.

Significance. If the reported results hold, the paper makes several useful contributions: an objective FPV-based evaluation protocol with both syntax and functional equivalence checking, the largest NL2SVA evaluation dataset to date, a synthetic fine-tuning dataset with structured explanations, and a multi-component RAG design that is more task-specific than generic RAG. The fine-tuning result on a 7B-parameter model is practically relevant for resource-constrained settings. However, the central empirical claims rest on an evaluation set that overlaps potentially with the training corpus and on a self-constructed benchmark, so the significance is conditional on resolving the data-leakage and external-validity concerns detailed below.

major comments (5)
  1. [III-B, III-C, IV-E, Table III, Appendix A] No deduplication is reported between the 4,070 textbook-derived training SVAs (Section III-B) and the 229 evaluation SVAs (Section III-C). Appendix A shows evaluation examples from OR1200, I2C, Wishbone, and an arbiter, all of which are standard designs likely to appear in the 67 hardware-design textbooks used for training. If the same or near-identical golden SVA appears in both corpora, the model can memorize answers rather than learn NL2SVA, directly inflating the 59.05% FM improvement claimed in the abstract. The authors should provide a concrete overlap analysis at the level of normalized SVA text, (design, signal, property) tuples, or both, and should re-run the fine-tuning experiments after excluding all overlapping or near-duplicate assertions. This is the most load-bearing test of the paper's main contribution.
  2. [III-C, IV-A] The evaluation dataset is constructed by the authors, and the natural-language property descriptions are manually written from the golden SVAs. The paper states in Section III-C that these descriptions 'do not contain any detailed signals,' but it does not report inter-annotator agreement, independent validation, or a comparison against existing benchmarks such as FVEval or AssertionBench. Because the synthetic fine-tuning explanations are also generated from golden SVAs, the test distribution may align with the training distribution in style and difficulty. I recommend evaluating on at least one external benchmark with independently authored property descriptions, and reporting the same FM/SC metrics there, to support the claim that the improvements generalize beyond the authors' own dataset.
  3. [IV-E, Table III] Table III shows that SVA operator-based rechecking decreases FM on the base Qwen model, from 105 FM with plain LLM to 101 FM with SOR, and that the full RAGSVAG framework also yields 101 FM. In contrast, HybridRetrieval alone improves the base Qwen to 113 FM. This is inconsistent with the narrative in Section IV-D that the rechecking component helps improve functionality match, and it means the full customized RAG pipeline is not beneficial for Qwen. The paper should either explain this degradation (e.g., the rechecking prompt corrupts correct assertions) or restrict the claims about rechecking to the models where it actually helps.
  4. [IV-D, II-C] AssertLLM, which the paper identifies in Section II-C as the closest RAG-based NL2SVA baseline, is never evaluated in the comparison of Section IV-D. Since the paper's core claim is that a customized RAG framework outperforms generic RAG, omitting AssertLLM leaves the comparison incomplete. At minimum, the authors should benchmark AssertLLM on the same 229-SVA evaluation set, or include an ablation that replaces HybridRetrieval with generic RAG over the same database and prompts, so the contribution of the customization is directly measured.
  5. [IV-A, IV-E] All reported SC and FM counts are single-run values despite the use of stochastic decoding (temperature 0.6, top_p 0.95 for Qwen, and presumably nonzero temperature for the API models). Because the headline improvements are computed from exact counts (e.g., 105 to 167 FM), run-to-run variance could change the conclusions. The authors should repeat each configuration multiple times and report the mean and standard deviation or confidence intervals, or at least demonstrate that the reported differences are stable across a small number of seeds.
minor comments (6)
  1. [IV-B, IV-C, IV-D] Figures 9, 10, and 11 are referenced in the text but do not appear in the manuscript; the numeric values for all baseline and ablation conditions should be included in tables or in the figure captions so the results are verifiable.
  2. [Abstract, IV-D] The abstract's 58.42% improvement is relative to GPT-4o-mini, but the absolute FM counts for the baseline and the improved model are not stated in the text; adding these numbers would make the headline result easier to interpret.
  3. [IV-E] The paper reports that Qwen-Finetune, trained on plain (SVA, explanation) pairs, regresses relative to the base model (87 FM vs. 105 FM). The conclusion that 'combining our customized RAG framework with prompt-guided fine-tuning delivers marked improvements' applies only to Qwen-Prompt-Finetune, not to Qwen-Finetune; the text should be more explicit about this distinction.
  4. [Table III] The caption uses 'customised' while the rest of the paper uses 'customized'; please standardize the spelling.
  5. [IV-D] The phrase 'enhance the FC accuracy' should read 'enhance the FM accuracy'.
  6. [III-C, IV-A] No link or repository is provided for the evaluation dataset or the fine-tuning dataset; an availability statement with URLs would be needed for reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central FM claims are checked by an external formal equivalence tool, and no load-bearing step reduces to its own inputs by construction.

full rationale

The paper's central claims—RAG and fine-tuning improve NL2SVA—are evaluated by Cadence JasperGold FPV equivalence between LLM-generated SVAs and golden SVAs (Section IV-A: 'we create the checking SVA by combining the property expression in the golden SVA with that in the LLM-generated SVA using SVA operator iff'). This is an external, objective check, not a quantity fitted from the model's own outputs. The RAG database is built from separate SystemVerilog textbooks (Section III-A1), the fine-tuning corpus from 67 textbooks (Section III-B), and the evaluation set from open-source cores and academic verification courses (Section III-C); no claim in the paper defines the evaluation outcome in terms of the training data. The manual NL annotations in the evaluation set are generated from the golden SVAs, and the fine-tuning explanations are also NL renderings of SVAs, which creates a potential style-overlap/generalization concern; likewise, no deduplication between the 4070 textbook SVAs and 229 evaluation SVAs is reported. These are benchmark-validity risks, not demonstrated circularity: the reported FM numbers could in principle be inflated by memorization, but the paper does not exhibit any equation or fitted parameter that makes an improvement true by construction. The only self-citation ([6], which shares author Karri) is a related-work pointer and is not load-bearing.

Assumptions & free parameters 6 free parameters · 5 assumptions · 0 invented entities

This is an empirical systems paper, so the ledger lists the design choices and unverified assumptions that the reported improvements depend on. No new physical or mathematical entities are introduced.

free parameters (6)
  • Fine-tuning learning rate = 8e-5
    Used for both Qwen fine-tuning variants; no sensitivity analysis or tuning reported. The result may depend on this choice.
  • Fine-tuning epochs = 3
    Fixed at three epochs; no grid search, so the reported improvements may not be optimal or robust.
  • Inference temperature = 0.6
    Used for Qwen model generation; not swept, so results could vary with temperature.
  • Inference top_p = 0.95
    Used for Qwen model generation; not swept.
  • Retrieval top_k = unspecified
    The number of chunks retrieved by HybridRetrieval is not stated; a key RAG hyperparameter that affects context quality.
  • Number of RAG textbooks = 10
    Retrieval database built from 10 textbooks; choice not justified and not varied.
assumptions (5)
  • domain assumption The manually written natural language properties in the evaluation set are faithful, representative specifications of the intended SVA behaviors.
    Section III-C states the properties are 'generated manually' without an independent validation process. If they are not representative of real NL2SVA descriptions, the reported FM improvements may not generalize.
  • domain assumption The synthetic fine-tuning dataset generated by OpenAI o4-mini accurately explains each SVA and its layer-by-layer construction.
    Section III-B describes using o4-mini to produce explanations and prompt-guided traces, with no human verification of correctness. Incorrect explanations would teach the model wrong mappings.
  • domain assumption The FPV-based iff equivalence correctly determines functional equivalence between generated and golden SVAs.
    Section IV-A constructs a checking assertion with iff. This is standard practice, but it assumes the golden SVA is itself correct and that the FPV tool's proof is sound for all 229 cases.
  • domain assumption The 40 Verilog designs and 229 SVAs are representative of the NL2SVA task.
    The dataset is drawn from open-source cores and academic courses, but no diversity analysis is provided. If the set is narrow, improvements may not transfer to other designs.
  • domain assumption The retrieval database built from 10 hardware verification textbooks contains relevant operator examples for the 40 evaluation designs.
    The paper does not verify coverage of the evaluation designs in the textbook corpus; if the designs are outside the textbook material, RAG may provide little relevant context.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA." pith.science (2026). https://pith.science/paper/4BPRN6BC

@misc{pith2026250621569,
  author       = {Pith},
  title        = {Pith review of: Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4BPRN6BC}},
  note         = {Machine review of arXiv:2506.21569}
}
read the original abstract

SystemVerilog Assertions (SVAs) are critical for verifying the correctness of hardware designs, but manually writing them from natural language property descriptions, i.e., NL2SVA, remains a labor-intensive and error-prone task. Recent advances in large language models (LLMs) offer opportunities to automate this translation. However, existing models still struggle with understanding domain-specific syntax and semantics. To enhance LLM performance in NL2SVA, we propose a customized retrieval-augmented generation (RAG) framework and a synthetic fine-tuning dataset that together improve LLM's performance. To further improve lightweight models over NL2SVA, our fine-tuning dataset provides prompt-guided explanations that teach LLMs the layer-by-layer construction process of concurrent SVAs, enabling supervised fine-tuning that greatly improves syntax and functionality accuracy. To evaluate the performance of LLMs over NL2SVA, we construct the largest evaluation dataset for NL2SVA, comprising 40 Verilog designs and 229 formally verified SVAs with detailed annotations. Experimental results show that our customized RAG framework increases the number of functionality matched SVAs by 58.42% over GPT-4o-mini, while Qwen2.5-Coder-7B-Instruct fine-tuned on our fine-tuning dataset and integrated with HybridRetrieval achieves a 59.05% over the base Qwen model.

Figures

Figures reproduced from arXiv: 2506.21569 by the authors.

Figure 1
Figure 1. Four layers of an example concurrent assertion. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Initial SVA generation prompt. LLM Assertion Assertion Specification Dynamic Splitting Technique￾based Database Customized RAG Hybrid Retrieval SVA Operator￾based Rechecking Refined LLM Assertion Initial SVA Generation Prompt Relevant Context Verilog [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Overall flow of the proposed customized RAG framework: apply [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (6 more)
Figure 6
Figure 6. Figure 6: SVA operators extraction prompt. [SVA Rechecking Prompt] Given the desired natural language property description [Natural Language Property description] Please check whether the following SystemVerilog assertion operates with the correct logic and timing, i.e., clock c…
Figure 9
Figure 9. Figure 9: Evaluation of dynamic splitting technique. [PITH_FULL_IMAGE:figures/full_fig_p005_9.png]
Figure 10
Figure 10. Figure 10: Evaluation of HybridRetrieval. StaticRAG (21.8%). However, both DynamicRAG and StaticRAG just achieve a slight improvement on SC over LLM. For DeepSeek, DynamicRAG and StaticRAG even degrade the performance of FM and SC slightly compared to the basic LLM. This behavio…
Figure 11
Figure 11. Figure 11: Evaluation and comparison of Customized RAG Framework. [PITH_FULL_IMAGE:figures/full_fig_p006_11.png]
Figure 12
Figure 12. Figure 12: Prompt for generating the prompt-guided explanation. [PITH_FULL_IMAGE:figures/full_fig_p009_12.png]
Figure 13
Figure 13. Figure 13: An example prompt-guided explanation [PITH_FULL_IMAGE:figures/full_fig_p010_13.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification

    cs.AR 2026-03 unverdicted novelty 7.0 of 10

    FVRuleLearner retrieves learned operator-level reasoning rules to boost the functional correctness of LLM-generated SystemVerilog assertions by roughly 30 percentage points over simple prompting baselines.

Reference graph

Works this paper leans on

30 extracted references · 27 canonical work pages · cited by 1 Pith paper

  1. [1]

    A survey on assertion-based hardware verification,

    H. Witharana et al., “A survey on assertion-based hardware verification,” ACM Comput. Surv., vol. 54, no. 11s, pp. 1–33, 2022

    work page 2022

  2. [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–2017 , pp. 1–1315, 2018

    work page 2017

  3. [3]

    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 DATE, 2010, pp. 626–629

    work page 2010

  4. [4]

    Automated generation of security assertions for rtl models,

    H. Witharana, A. Jayasena, A. Whigham, and P. Mishra, “Automated generation of security assertions for rtl models,” J. Emerg. Technol. Comput. Syst., vol. 19, no. 1, 2023

    work page 2023

  5. [5]

    Generative AI assertions in UVM-based system verilog functional verification,

    V . Radu et al., “Generative AI assertions in UVM-based system verilog functional verification,” Systems, vol. 12, no. 10, 2024

    work page 2024

  6. [6]

    ChI- RAAG: ChatGPT informed rapid and automated assertion generation,

    B. Mali, K. Maddala, V . Gupta, S. Reddy, C. Karfa, and R. Karri, “ChI- RAAG: ChatGPT informed rapid and automated assertion generation,” in IEEE Computer Society Annual Symposium on VLSI , 2024, pp. 680– 683

    work page 2024

  7. [7]

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

    Z. Yan et al., “AssertLLM: Generating hardware verification assertions from design specifications via multi-llms,” in ASP-DAC, 2025, pp. 614– 621

    work page 2025

  8. [8]

    SpecToSV A: Circuit specification document to systemverilog assertion translation,

    G. Parthasarathy, S. Nanda, P. Choudhary, and P. Patil, “SpecToSV A: Circuit specification document to systemverilog assertion translation,” in Second Document Intelligence Workshop at KDD , 2021

    work page 2021

Show all 30 references
  1. [9]

    NSPG: Natural language processing-based security property generator for hardware security assurance,

    X. Meng et al. , “NSPG: Natural language processing-based security property generator for hardware security assurance,” in DAC, 2024, pp. 1–6

    2024

  2. [10]

    GLAsT: Learning formal grammars to translate natural language specifications into hardware assertions,

    C. B. Harris and I. G. Harris, “GLAsT: Learning formal grammars to translate natural language specifications into hardware assertions,” in DATE, 2016, pp. 966–971

    2016

  3. [11]

    EASE: Enabling hardware assertion synthesis from english,

    R. Krishnamurthy and M. S. Hsiao, “EASE: Enabling hardware assertion synthesis from english,” in RuleML+RR, 2019, pp. 82–96

    2019

  4. [12]

    nl2spec: Interactively translating unstructured natural language to temporal logics withlarge language models,

    M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics withlarge language models,” in Computer Aided Verification, 2023, pp. 383–396

    2023

  5. [13]

    Spec2Assertion: Automatic pre-RTL assertion generation using large language models with progressive regularization,

    F. Wu et al., “Spec2Assertion: Automatic pre-RTL assertion generation using large language models with progressive regularization,” arXiv preprint arXiv:2505.07995, 2025

    2025 arXiv

  6. [14]

    Automatic high-quality verilog assertion generation through subtask-focused fine- tuned LLMs and iterative prompting,

    M. Shahidzadeh, B. Ghavami, S. Wilton, and L. Shannon, “Automatic high-quality verilog assertion generation through subtask-focused fine- tuned LLMs and iterative prompting,” arXiv, 2024

    2024

  7. [15]

    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-2023 (Revision of IEEE Std 1800-2017), pp. 1–1354, 2024

    2023

  8. [16]

    Retrieval-augmented generation for knowledge-intensive NLP tasks,

    P. Lewis et al., “Retrieval-augmented generation for knowledge-intensive NLP tasks,” in Advances in neural information processing systems, 2020, pp. 9459–9474

    2020

  9. [17]

    LLM-based and retrieval-augmented control code generation,

    H. Koziolek et al. , “LLM-based and retrieval-augmented control code generation,” in International Workshop on Large Language Models for Code, 2024, pp. 22–29

    2024

  10. [18]

    Benchmarking retrieval- augmented generation for medicine,

    G. Xiong, Q. Jin, Z. Lu, and A. Zhang, “Benchmarking retrieval- augmented generation for medicine,” in Association for Computational Linguistics, 2024, pp. 6233–6251

    2024

  11. [19]

    Improving retrieval for RAG based question answering models on financial doc- uments,

    S. Setty, H. Thakkar, A. Lee, E. Chung, and N. Vidra, “Improving retrieval for RAG based question answering models on financial doc- uments,” arXiv, 2024

    2024

  12. [20]

    Toward con- versational agents with context and time sensitive long-term memory,

    N. Alonso, T. Figliolia, A. Ndirango, and B. Millidge, “Toward con- versational agents with context and time sensitive long-term memory,” arXiv, 2024

    2024

  13. [21]

    ChunkRAG: Novel LLM-chunk filtering method for rag systems,

    I. Singh et al., “ChunkRAG: Novel LLM-chunk filtering method for rag systems,” arXiv, 2024

    2024

  14. [22]

    MAIN-RAG: Multi-Agent Filtering Retrieval- Augmented Generation,

    C. Chang et al. , “MAIN-RAG: Multi-Agent Filtering Retrieval- Augmented Generation,” arXiv, 2024

    2024

  15. [23]

    Don’t forget to connect! improving rag with graph-based reranking,

    J. Dong, B. Fatemi, B. Perozzi, L. Yang, and A. Tsitsulin, “Don’t forget to connect! improving rag with graph-based reranking,” arXiv, 2024

    2024

  16. [24]

    AssertionBench: A benchmark to evaluate large-language models for assertion generation,

    P. Vaishnavi, N. Deeksha, D. Soham, and P. Debjit, “AssertionBench: A benchmark to evaluate large-language models for assertion generation,”

  17. [25]

    FVEval: Understanding language model capabilities in formal verification of digital hardware,

    K. Minwoo et al., “FVEval: Understanding language model capabilities in formal verification of digital hardware,” 2024. [Online]. Available: https://arxiv.org/abs/2410.23299

    2024 arXiv

  18. [26]

    Cadence JasperGold Formal Verification Platform,

    C. D. Systems, “Cadence JasperGold Formal Verification Platform,”

  19. [27]

    Qwen2. 5-coder technical report,

    B. Hui et al., “Qwen2. 5-coder technical report,” arXiv, 2024

    2024

  20. [28]

    Llamafactory: Unified efficient fine-tuning of 100+ language models,

    Y . Zheng et al. , “Llamafactory: Unified efficient fine-tuning of 100+ language models,” in ACL, 2024. APPENDIX A. Example SVAs Across all 10 examples in Table IV, the SV As generated by our customized RAG framework pass the functionality verification, meaning they accurately...

    2024

  21. [2023]

    Available: https://www.cadence.com/

    [Online]. Available: https://www.cadence.com/

  22. [2025]

    Available: https://arxiv.org/abs/2406.18627

    [Online]. Available: https://arxiv.org/abs/2406.18627

    arXiv

Pith tools

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