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_ENGPRES028@linklings.com
SUMMARY:Formally Validating Industry Standard BCH‑ECC/CRC Codes – A Step b
 y Step Recipe
DESCRIPTION:Disha Puri and Aatreyi Bal (Synopsys)\n\nFormal verification o
 f CRC and ECC hardware does not scale with conventional techniques due to 
 large Datapath's, extensive lookup tables, and complex Galois-field arithm
 etic. Existing approaches rely on monolithic end-to-end properties, bounde
 d proofs, or coarse linearity abstractions, and even then, they typically 
 break down beyond ~512-bit widths.\n\nThis paper introduces a theorem-guid
 ed formal verification methodology that scales to production-class CRC and
  ECC designs. The key novelty is a systematic decomposition of functional 
 correctness into reusable, mathematically grounded theorems capturing stru
 ctural and algebraic invariants—such as linearity, syndrome correctness an
 d consistency, and error-propagation properties of locator polynomials. Th
 ese theorems are proved independently, and proof is composed of incrementa
 lly using assume–guarantee reasoning within an industry-standard formal to
 ol (VC Formal).\n\nWe have validated the approach on two industrial design
 s: an IEEE 802.3 CRC with a 5120-bit pipelined Datapath, and a BCH DECTED 
 ECC with m = 2047 and t = 2. Prior methods time out, whereas our methodolo
 gy achieves complete functional verification. \n\nTo our knowledge, this i
 s the first demonstration of scalable and complete formal verification of 
 CRC/ECC designs at this scale using a production-ready formal tool, making
  the approach directly applicable to industrial verification flows.\n\nTop
 ics: AI, Chiplet, Design, EDA, Quantum, Security, Systems\n\n
END:VEVENT
END:VCALENDAR