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:20240626T180033Z
LOCATION:Level 2 Lobby
DTSTART;TZID=America/Los_Angeles:20240626T180000
DTEND;TZID=America/Los_Angeles:20240626T190000
UID:dac_DAC 2024_sess256_LBR112@linklings.com
SUMMARY:Late Breaking Results: LLM-assisted Automated Incremental Proof Ge
 neration for Hardware Verification
DESCRIPTION:Late Breaking Results Poster\n\nKhushboo Qayyum, Muhammad Hass
 an, Sallar Ahmadi-Pour, Chandan Kumar Jha, and Rolf Drechsler (University 
 of Bremen)\n\nIn this paper, we propose a methodology for hardware verific
 ation assisted by Large Language Models (LLMs) in the incremental proof ge
 neration process. First, an LLM identifies the basic module of the Design 
 Under Verification (DUV), followed by expanding the proof scope as more mo
 dules are added. LLMs assist in defining and verifying invariants for each
  module using the Z3 solver, and in formulating integration properties at 
 module interfaces. Our case studies on a Ripple Carry Adder and a Dadda Tr
 ee multiplier demonstrate that LLMs enhance the efficiency and accuracy of
  hardware verification.
END:VEVENT
END:VCALENDAR