Presentation
Multi-Agent Automated Formal Verification for Automative Applications
DescriptionWith the advent of AI and the rise of Software-Defined Vehicles (SDV), automotive designs are growing exponentially in complexity and functionality. Ensuring safety, security, and early bug detection is more critical than ever. A promising approach is combining AI with formal verification to achieve both productivity and exhaustive coverage. Recent advances in local Large Language Models (LLMs) make it feasible to generate syntactically and functionally correct assertions without exposing proprietary data to external servers, addressing privacy concerns associated with frontier models.
This work proposes a multi-agent system using local LLMs to automate formal verification setup for digital IPs. Inputs include RTL filelists, assertion specifications, and a chosen formal technique. To simplify complexity, predefined "modes" guide the master agent with context-specific prompts (e.g., symbolic-data-checker mode). Specialized agents then: (1) create a formal testbench, (2) identify relevant DUT signals, (3) generate auxiliary code for symbolic variables and assumptions, (4) connect signals to symbolic variables, and (5) produce final assertions. An optional step validates syntax and provides feedback for refinement. The proposed tool supports multiple modes, aiming to improve formal checker quality and streamline verification flows for diverse IPs in the automotive domain.
This work proposes a multi-agent system using local LLMs to automate formal verification setup for digital IPs. Inputs include RTL filelists, assertion specifications, and a chosen formal technique. To simplify complexity, predefined "modes" guide the master agent with context-specific prompts (e.g., symbolic-data-checker mode). Specialized agents then: (1) create a formal testbench, (2) identify relevant DUT signals, (3) generate auxiliary code for symbolic variables and assumptions, (4) connect signals to symbolic variables, and (5) produce final assertions. An optional step validates syntax and provides feedback for refinement. The proposed tool supports multiple modes, aiming to improve formal checker quality and streamline verification flows for diverse IPs in the automotive domain.
Event Type
Engineering Poster
TimeMonday, July 275:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor