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:20260402T024533Z
LOCATION:Engineering Posters\, Level 2 Exhibit Hall
DTSTART;TZID=America/Los_Angeles:20250624T170000
DTEND;TZID=America/Los_Angeles:20250624T180000
UID:dac_DAC 2025_sess264_ENGPOST175@linklings.com
SUMMARY:Approach For Quality DV Using C2RTL For Algorithmic Designs Author
 s: Neema Agarwal, Himanshu Chauhan, Harsh Setia, Atharva Mahesh Kakde, Ket
 ki Gosavi
DESCRIPTION:Neema Agarwal (Samsung); Himanshu Chauhan and Harsh Setia (Sam
 sung Semiconductor); and Atharva Kakde and Ketki Gosavi (Cadence Design Sy
 stems, Inc.)\n\nData path design with algorithmic logic have their own cha
 llenges in verification. DV sign off using simulation alone can have holes
  as it is nearly impossible to cover all scenarios in limited DV time fram
 e. By formally verifying the equivalence check between RTL and its referen
 ce C++ model algorithm provides an edge over traditional simulation approa
 ch. The paper describes the advantages of using C2RTL equivalence for this
  verification.\n\nDesign Use Case-De-Compression IP:\n\nThe decompression 
 IP uses the LZO RLE algorithm for decompressing the data up to 4KB Input c
 ompressed data stream, can have input size between 19 bytes to 4KB which m
 akes it difficult to cover all input data values with functional simulatio
 n. This can lead to some uncovered scenarios in algorithm and hence bug es
 capes.\n\nApproach Taken:\n\n1) Instruction based formal verification\n\n2
 ) Reduced number of properties in FV setup\n\n3) Unique Mapping Requiremen
 t of C variables with RTL cycle-based signal\n\nResults:\n\nVerified 3 ran
 dom instructions sequence with Input vector size ranging from 19 – 64 byte
 s. This resulted in a failure case.\n\n   Compressed Input data 60 bytes i
 nsize: 240'h00000000d09002000a360088004010111\n\n   Decompressed Output Da
 ta:\n\n        RTL Output: 128'h0000 0009 0020 6060 6060 6060   6008 8004\
 n\n        C++ Output: 128'h0020 6009 0020 6060 6060 6060   6008 8004\n\nA
 fter analyzing the LZO algorithm encoding of compressed instruction, C++ d
 ecompressed output data is correct, but RTL output data is incorrect. This
  could not be covered in simulation-based approach even when thousands of 
 input vectors were simulated for more than a month to decompressor RTL.\n\
 nTopics: Front-End Design\n\n
END:VEVENT
END:VCALENDAR