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:20260730T152640Z
LOCATION:Exhibit Hall
DTSTART;TZID=America/Los_Angeles:20260728T172300
DTEND;TZID=America/Los_Angeles:20260728T172300
UID:dac_DAC 2026_sess306_WIP757@linklings.com
SUMMARY:A novel way to handle non-convergence of properties in formal veri
 fication of digital systems
DESCRIPTION:surinder sood, kishan mushar, and Nirmal Jose (ARM)\n\nThe inc
 reasing complexity of modern digital designs presents significant challeng
 es for formal verification, particularly when properties fail to converge 
 within practical proof bounds. Non-convergent assertions hinder verificati
 on sign-off and limit the ability to expose deep corner-case bugs. This wo
 rk proposes a contract-based refinement framework to enhance property conv
 ergence in the formal verification of complex hardware systems. The method
 ology employs proof decomposition to identify refinement properties—helper
  assertions selected through overlapping cones of influence (COI)—which ar
 e then composed to strengthen the convergence of the target property. Impl
 emented and evaluated using the Cadence JasperGold formal verification pla
 tform, the approach demonstrates improved proof bounds and enhanced bug de
 tection across multiple architectures, including memory controllers and CP
 Us. Results show that the proposed technique systematically improves conve
 rgence for critical properties while maintaining scalability and broad app
 licability to diverse digital designs.\n\nTrack: Student\n\n
END:VEVENT
END:VCALENDAR