BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Denver
X-LIC-LOCATION:America/Denver
BEGIN:DAYLIGHT
TZOFFSETFROM:-0700
TZOFFSETTO:-0600
TZNAME:MDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0600
TZOFFSETTO:-0700
TZNAME:MST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260422T000713Z
LOCATION:505
DTSTART;TZID=America/Denver:20231115T153000
DTEND;TZID=America/Denver:20231115T153900
UID:submissions.supercomputing.org_SC23_sess308_spostg111@linklings.com
SUMMARY:A Formal Specification of Tensor Cores via Satisfiability Modulo T
 heories
DESCRIPTION:Benjamin Valpey (University of Rochester)\n\nIn this work, we 
 explore how to replicate the behavior of undocumented hardware units -- in
  this case, NVIDIA's Tensor Cores -- and reason about them.\n\nWhile prior
  work has employed manual testing to identify hardware behavior, we show t
 hat SMT can be used to generate inputs that can discriminate between diffe
 rent hardware implementation choices. We argue that SMTLIB, the language s
 pecification for SMT solvers, is well suited for exposing hardware impleme
 ntations.\n\nUsing our method, we create a formal specification of the ten
 sor cores on NVIDIA's Volta architecture. We confirm many of the findings 
 of previous studies on tensor cores, but also identify two discrepancies: 
 we find that the hardware does not use IEEE-754 round-to-zero for accumula
 tion and that the 5-term accumulator requires 3 extra bits for carry out s
 ince it does not normalize intermediate sums.\n\nThe work will be presente
 d in person using the poster as a visual aid.\n\nRegistration Category: Te
 ch Program Reg Pass\n\nSession Chair: Ana Gainaru (Oak Ridge National Labo
 ratory (ORNL))\n\n
END:VEVENT
END:VCALENDAR