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:20260729T150000
DTEND;TZID=America/Los_Angeles:20260729T160000
UID:dac_DAC 2026_sess296_ENGPOST452@linklings.com
SUMMARY:Formal Verification Engineering for Integer Vector Neural Network 
 Instructions
DESCRIPTION:Jaideep Ramachandran and Roope Kaivola (Intel)\n\nIntel has be
 en doing full formal verification of CPU execution datapaths for over 25 y
 ears. We present as a case study in verification engineering, the formal v
 erification of the integer subset of VNNI instruction set that was introdu
 ced as part of Intel Deep Learning Boost. An example of an Int16 SIMD MUL 
 (SiMUL) VNNI instruction is VPDPWSSD, which multiplies the individual sign
 ed words of the first source operand by the corresponding signed words of 
 the second source operand, producing intermediate signed, doubleword resul
 ts. The adjacent doubleword results are then summed and accumulated in the
  destination operand. These Int16 and Int8 instructions come in different 
 flavors based on whether sources are signed or unsigned, and whether the i
 ntermediate sums on overflowing are saturated to maximum magnitude with th
 e correct sign, for the result. The underlying FV engine is powered by sym
 bolic simulation, which provides the verification engineer the ability to 
 concretely debug verification complexity, and the ability to program aroun
 d verification complexity. Our verification flow built on top of symbolic 
 simulation using "FV as first class software" approach has enabled us to d
 evelop flexible, reusable proofs while providing full data space coverage 
 for all flavors of SiMUL VNNI instructions.\n\nTopics: AI, Chiplet, Design
 , EDA, Quantum, Security, Systems\n\n
END:VEVENT
END:VCALENDAR