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:20260730T152729Z
LOCATION:Seaside Ballroom B
DTSTART;TZID=America/Los_Angeles:20260728T104500
DTEND;TZID=America/Los_Angeles:20260728T110000
UID:dac_DAC 2026_sess272_ENGPRES445@linklings.com
SUMMARY:No Credit Where Credit Is Due: Quiesced Formal Check for PCIe Cred
 iting
DESCRIPTION:Isha Lale, Pradip Prajapati, and Anshul Jain (Synopsys)\n\nPCI
 e Gen6/7 introduces major architectural enhancements to meet the bandwidth
  and latency demands of AI and datacentre workloads. Bandwidth doubles fro
 m 32 GT/s to 64 GT/s to 128GT/s through support for PAM4 signalling, flit‑
 based transfers, and multiple virtual channels (VCs). These capabilities a
 lso significantly increase the complexity of credit management, which gove
 rns buffer availability between transmitter and receiver. Gen6 onwards, ea
 ch VC maintains its own dedicated credits while additionally drawing from 
 a dynamic pool of shared credits. Features such as infinite credits and me
 rged‑credit modes further expand the state space, making correct credit ha
 ndling essential for avoiding pipeline deadlock, VC starvation, and silent
  throughput loss.\nTraditional simulation‑driven approaches are unable to 
 exhaustively explore the combinatorial explosion of credit configurations,
  buffer‑availability permutations, and multi‑TLP corner cases. To address 
 this gap, we propose a quiescence‑based formal verification methodology ai
 med at proving forward progress for all in‑flight TLPs whenever sufficient
  receiver credits are available. The method isolates the design by suppres
 sing external stimuli and driving the system toward a stable quiesced stat
 e. It uses symbolic TLPs, precise modelling of PCIe credit semantics, and 
 quiescence‑driven stabilization proofs to ensure that forward progress is 
 guaranteed under all legal credit scenarios.\nApplying this methodology un
 covered a subtle but critical bug in credit revaluation logic—an issue dee
 ply buried in mode‑transition sequences and effectively unreachable throug
 h conventional verification. Our results show that quiesced formal verific
 ation provides exhaustive coverage of credit modes, exposes otherwise‑inac
 cessible corner‑case failures, and delivers high‑certainty correctness for
  next‑generation PCIe interconnect designs.\n\nTopics: Design, EDA, System
 s\n\nSession Chair: Nanditha Rao (IBM)\n\n
END:VEVENT
END:VCALENDAR