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:20260730T152730Z
LOCATION:DAC Pavilion\, Exhibit Floor
DTSTART;TZID=America/Los_Angeles:20260728T170000
DTEND;TZID=America/Los_Angeles:20260728T180000
UID:dac_DAC 2026_sess295_ENGPOST257@linklings.com
SUMMARY:Breaking Sequential Depth Barriers: An FSM-Driven Bridge for the F
 ormal Verification of Virtually Address-Mapped Hardware Registers
DESCRIPTION:Sarvesh TIWARI, Ayush ., and Ashwin Singhal (STMicroelectronic
 s) and Tom Weiss and Erik Seligman (Cadence Design Systems, Inc.)\n\nThis 
 paper presents the formal verification of a subsystem with indirect read m
 echanisms and a nonstandard access protocol. Verifying registers using the
  control and status register (CSR) protocol typically requires a proof acc
 elerator to convert a standard bus into the CSR protocol. However, this se
 cure design uses a custom protocol, creating unique formal verification ch
 allenges. In this design, writing to an IP register through the subsystem 
 is straightforward and followed by polling a status register to check the 
 write data status. The read data is available at a different address withi
 n the subsystem register map.\nTo address this, a protocol-to-protocol AMB
 A bridge is developed. The bridge converts write commands from the verific
 ation intellectual property (VIP) into writes for the device under test (D
 UT) and reads data from the DUT, returning it to the corresponding VIP add
 ress. Because the DUT does not return data at the same address, address co
 nversion logic with several finite state machines (FSMs) is implemented. T
 his approach allows the VIP to perform checks as expected, despite the ind
 irect read mechanism.\nCounter value abstraction is used to manage delays 
 and simplify verification, ensuring efficient completion. This approach en
 ables robust and efficient register verification for complex subsystems an
 d saves significant time compared with the UVM register model.\n\nTopics: 
 AI, Chiplet, Design, EDA, Quantum, Security, Systems\n\n
END:VEVENT
END:VCALENDAR