BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260730T152639Z
LOCATION:Exhibit Hall
DTSTART;TZID=America/Los_Angeles:20260728T170600
DTEND;TZID=America/Los_Angeles:20260728T170700
UID:dac_DAC 2026_sess306_WIP1573@linklings.com
SUMMARY:Will AI mess my RTL? A snapshot-based approach to verifying AI-wri
 tten RTL
DESCRIPTION:Bernat Homs and Oscar Palomar (Barcelona Supercomputing Center
 ), Miquel Moreto (BSC), and Marcelo Orenes-Vera (NVIDIA)\n\nWith the growi
 ng interest in using AI (Artificial Intelligence) for RTL (Register-Transf
 er Level) hardware development, robust and comprehensive verification has 
 become more important than ever. As Large Language Models (LLMs) increasin
 gly assist in creating and modifying RTL designs, ensuring that these chan
 ges preserve existing functionality is paramount for building trust in AI-
 driven workflows. We present SVApshot, a fully automated framework that le
 verages LLMs to generate and systematically attempt to correct SystemVeril
 og Assertions (SVA) for RTL modules, completely removing the human from th
 e generation loop. SVApshot introduces a novel snapshot methodology that c
 aptures the current functionality of a design as a comprehensive set of fo
 rmal assertions, creating a regression suite for validating future changes
 -whether made by humans or AI. The framework features automated duplicate 
 detection, assertion set expansion, and iterative repair of failing assert
 ions using LLM-guided debugging with formal verification feedback. Our exp
 erimental evaluation across diverse RTL  modules demonstrates high coverag
 e for complex modules, with successful detection of both manually-injected
  and AI-introduced bugs. Additionally, this framework opens the door for a
 utomatic generation of formal testbenches to benchmark LLMs for hardware d
 esign, moving beyond binary pass/fail metrics towards nuanced assertion-ba
 sed scoring.\n\nTrack: Student\n\n
END:VEVENT
END:VCALENDAR
