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:20240626T180034Z
LOCATION:2010\, 2nd Floor
DTSTART;TZID=America/Los_Angeles:20240624T141500
DTEND;TZID=America/Los_Angeles:20240624T143000
UID:dac_DAC 2024_sess190_FED032@linklings.com
SUMMARY:Breaking the Formal Convergence Barriers of a Floating-Point Dot-P
 roduct Block for AI/ML Accelerators
DESCRIPTION:Front-End Design\n\nSatyabrata Sarangi (Meta); Neelabja Dutta 
 (Synopsys); Sai Ma (Meta); Ashish Kapoor and Reily Jacoby (Synopsys); and 
 Adrian Lewis, Rohan Mallya, and Eda Sahin (Meta)\n\nDot-product compute en
 gines are pivotal to any of the AI/ML hardware accelerators. Multi-term an
 d floating-point dot-product engines increase the datapath complexity due 
 to added logic for rounding, normalization, and alignment of significands 
 per maximum exponent. To formally verify such dot-product compute engines,
  a C/C++ vs RTL formal check tool (e.g. Synopsys's VC Formal DPV) is used.
  The datapath complexity of a multi-term and floating-point dot-product en
 gine for a complex AI/ML chip along with different dataflow graph (DFG) st
 ructures of the corresponding C/C++ and RTL models often make it difficult
  for the formal tool to converge. This research depicts various techniques
  (assume-guarantee, lemma partitioning, DFG optimization, maximizing equiv
 alence points, case splitting, and using optimized solvers) that are adopt
 ed to obtain formal convergence across several floating-point types. Moreo
 ver, we enable helper lemmas after coming up with adder tree expressions t
 o match the RTL and C-model adder tree structures. The results demonstrate
  that a formal run for a multi-term FP32-based dot-product operation can c
 onverge within 30mins. We recommend a new feature for the VC Formal DPV to
 ol to streamline detection of the adder trees and automatically resolving 
 them in the flow, which Synopsys is currently working on.\n\nTopic: Design
 , Engineering Tracks, Front-End Design\n\nSession Chair: Puneet Anand (Qua
 lcomm)
END:VEVENT
END:VCALENDAR