Presentation
A Leap Forward in Formal Verification Using Generative AI
DescriptionGenerative AI has transformed various fields, including design verification, particularly formal verification (FV). FV is challenging due to its steep learning curve, especially in Formal Property Verification (FPV), which involves generating properties like assertions and assumptions in System Verilog Assertions (SVA). This process requires a deep understanding of the design and SVA syntax.
Generative AI can simplify this by creating SVA from prompts and RTL. It uses Large Language Models (LLMs) and Vector Databases (RAG) to streamline property generation. Ideally, an LLM fine-tuned with sufficient data can translate English to SVA in a design context, significantly easing the process. Even without fine-tuning, a robust RAG system with ample local data can provide relevant examples, working effectively with a generic LLM.
However, LLM responses can be error-prone, necessitating guardrails like compiler checks, linters, user feedback, and testbenches. The challenge lies in managing the numerous components: selecting the best LLM, the most supportive RAG system, effective prompts, and generating and updating the testbench. An incubator must evaluate and choose the right components for this experimentation.
Generative AI can simplify this by creating SVA from prompts and RTL. It uses Large Language Models (LLMs) and Vector Databases (RAG) to streamline property generation. Ideally, an LLM fine-tuned with sufficient data can translate English to SVA in a design context, significantly easing the process. Even without fine-tuning, a robust RAG system with ample local data can provide relevant examples, working effectively with a generic LLM.
However, LLM responses can be error-prone, necessitating guardrails like compiler checks, linters, user feedback, and testbenches. The challenge lies in managing the numerous components: selecting the best LLM, the most supportive RAG system, effective prompts, and generating and updating the testbench. An incubator must evaluate and choose the right components for this experimentation.
Event Type
Engineering Presentation
TimeTuesday, June 244:15pm - 4:30pm PDT
Location2010, Level 2
AI
Front-End Design
Chiplet
Similar Presentations