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:20260730T152639Z
LOCATION:DAC Pavilion\, Exhibit Floor
DTSTART;TZID=America/Los_Angeles:20260728T170000
DTEND;TZID=America/Los_Angeles:20260728T180000
UID:dac_DAC 2026_sess295_ENGPRES327@linklings.com
SUMMARY:Hardening Security of HW IPs by Verifying Their Negative Space For
 mally
DESCRIPTION:Sayak Ray, Jason Fung, Bo-Yuan Huang, Arun Kanuparthi, Mohamma
 d Bidmeshki, Mehdi Mohtashemi, Ramya Hariharan, and Vivek Tiwari (Intel)\n
 \nNegative space verification is crucial for hardware security: inputs tha
 t are invalid or unexpected can trigger silent and delayed failures that d
 esigners often treat as "don't care". These failures. If exploitable, can 
 cause security issues. We show that unlike software fuzzing, formal verifi
 cation (FV) is better suited for hardware negative space verification due 
 to hardware's hierarchical structure, structured inputs, and subtle failur
 e modes. Our recommended workflow uses Compliance Monitors to organize con
 straints and checks, with specific expertise deployed in selectively disab
 ling assumptions to enable a particular negative space. Custom properties 
 are used when Compliance Monitors are unavailable, or to mitigate state ex
 plosion. We applied this approach to three interface protocols across mult
 iple IPs: several IPs proved clean, early bugs were found and fixed in oth
 ers, and custom FV enabled efficient post-fix proofs. Benefits include red
 uced pre-silicon escape costs, faster IP-level verification turnaround, im
 proved specification clarity, and higher implementation quality. For cases
  where negative space specification is unavailable, we are experimenting w
 ith GenAI-based automatic negative specification mining, and our early res
 ults are encouraging. Attendees will learn practical patterns, choices, ho
 w to document and prove negative behaviors effectively and robustly, and o
 ur experiments with GenAI for mining negative space specification.\n\nTopi
 cs: AI, Chiplet, Design, EDA, Quantum, Security, Systems\n\n
END:VEVENT
END:VCALENDAR