RAG-assisted LLM-based Verification

Introduction

Large Language Models (LLMs) like GPT-4 and Claude have transformed how we generate and understand human-like language. However, they come with certain limitations:

• May hallucinate or generate inaccurate outputs
• Cannot access real-time or domain-specific external data
• Performance degrades in high-stakes or technical domains without training

Retrieval-Augmented Generation (RAG) addresses these limitations by combining LLMs with external search:

• A retriever selects relevant knowledge from a document store or database
• The LLM generates responses using the retrieved context

This project applies the RAG+LLM architecture to hardware verification and EDA workflows, enabling smarter, explainable, and more accurate analysis pipelines.

Project Overview

Large Language Models (LLMs) like GPT or LLaMA are impressive in language generation, but their general training data often lacks the precision and depth required for technical domains like Electronic Design Automation (EDA). This mismatch results in hallucinations and limited reasoning when applied to tasks like formal verification, waveform interpretation, or RTL debugging.

Our project addresses this limitation by integrating Retrieval-Augmented Generation (RAG) into the LLM pipeline. By connecting LLMs to a curated knowledge base of EDA documents—such as SystemVerilog assertions, waveform logs, and simulation outputs—we empower them to reason with up-to-date, accurate, and domain-specific information.

This hybrid system not only improves factual accuracy but also introduces transparency through Explainable AI (XAI) techniques, offering insights into how the model arrived at each conclusion. Whether it’s detecting design bugs or suggesting testbench improvements, this tool represents a leap forward in intelligent automation for chip design.

Explore the source code, architecture, and example queries on our GitHub repository.

Architecture Snapshot

(Coming soon!) We'll upload the end-to-end RAG+LLM pipeline diagram that illustrates:

• LangChain or RAG backend
• Interaction with Z3 SMT solver or Verilog test cases
• Human-in-the-loop debugging

Related Technologies

• LLMs (GPT-4, Claude, LLaMA)
• LangChain
• SystemVerilog + Assertions (SVA)
• Z3 Theorem Prover
• Word2Vec + LDA (for semantic drift detection)

📚 Research Papers

1. Dataset

• VERT: A SystemVerilog Assertion Dataset to Improve Hardware Verification with LLMs
• AssertionBench: A Benchmark for LLMs in Assertion Generation
• OpenLLM-RTL: Open Dataset & Benchmark for RTL Generation
• VerilogDB: Preprocessed Dataset for LLM RTL Generation

2. LLM Verification

• LLM Verification
• LLMs for Hardware Verification
• LLM-Guided Formal Verification
• AssertLLM: Assertion Generation with Multi-LLMs
• Continual Learning of LLMs – Survey
• Incremental Learning in LLMs – Critical Review

3. Explainable AI (XAI)

• Survey on Concept Drift Monitoring
• Unsupervised Drift Detection – Benchmark and Survey

4. Foundational & Other Papers

• Word2Vec – Google Research
• Attention Is All You Need
• Retrieval-Augmented Generation (RAG) – Facebook AI
• LLaMA: Open and Efficient Foundation Models – Meta AI
• HybridRAG: Knowledge Graph + Vector Retrieval
• Topic Evolution with LDA + Word2Vec

Contact

Questions or collaborations? Reach out via GitHub or email: maheshsadupalli [at] gmail.com