Tags:Assertion-based Verification (ABV), Automated-Assertion Generation, Bounded Model Checker (BMC), Designer-tailored Specifications, High-Level Specifications, Large Language Models (LLMs), Retrieval-Augmented Generation (RAG), SystemVerilog Assertions (SVAs) and VLSI Design Flow
Abstract:
Assertion-based verification (ABV) is widely used in VLSI design. However, manual assertion writing is time-consuming and may not adhere to high-level specifications. Generative AI techniques like LLMs automate this but can introduce hallucination. We propose an automatic assertion generation framework using Retrieval-Augmented Generation (RAG) and LLMs. It generates assertions from designer-tailored specifications, ensuring conformance with high-level specifications and reducing hallucinations. We applied this to an AXI4-Lite protocol case study, verifying SystemVerilog Assertions (SVAs) against golden RTL using Bounded Model Checking (BMC). Results showed improved accuracy, conformance, and integration with ABV.
Enhanced VLSI Assertion Generation: Conforming to High-Level Specifications and Reducing LLM Hallucinations with RAG