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:20240626T180033Z
LOCATION:2010\, 2nd Floor
DTSTART;TZID=America/Los_Angeles:20240625T140000
DTEND;TZID=America/Los_Angeles:20240625T141500
UID:dac_DAC 2024_sess191_FED010@linklings.com
SUMMARY:Enhancing Quality and Reducing Verification Effort for RTL Impleme
 ntations against High-Level C/C++ Models using Formal Equivalence
DESCRIPTION:Front-End Design\n\nDavid Vincenzoni and Gianluca Rigano (STMi
 croelectronics) and Gaetano Raia and Maurizio Martina (Politecnico di Tori
 no)\n\nThe complexity of modern System on Chip (SoC) designs has led to ad
 vanced verification techniques, facing the challenge of detecting undetect
 ed functional failures.\n\nIn the area of wireless and wireline communicat
 ion products, designers initially model Digital Signal Processing (DSP) bl
 ocks using high-level languages like MATLABŪ or C/C++. Subsequently, they 
 translate these models into Register Transfer Level (RTL) implementations.
  Traditional verification methods involve months-long Universal Verificati
 on Methodology (UVM) dynamic simulations, yet subtle bugs in critical DSP 
 blocks can remain hidden.\n\nTo address this, Formal Equivalence Verificat
 ion (FEV) emerges as a powerful complement to dynamic simulations. Thanks 
 to recent improvements in the capabilities of formal solvers, FEV offers a
  unique advantage by mathematically checking the functional correctness of
  an RTL implementation (timed) against its high-level C/C++ model (untimed
 ), drastically reducing verification time, and ensuring exhaustive coverag
 e of the design state space.\n\nThis paper presents an in-depth exploratio
 n of complex FSM with Datapath verification, namely Floating-Point MAC, To
 ne Generator, and Automatic Gain Control, utilizing Formal Equivalence met
 hodology. Despite these DSP blocks had been validated throughout UVM dynam
 ic simulations which lasted months, subtle corner cases hidden bugs were s
 potted in few weeks by adopting the proposed flow, therefore reducing the 
 verification effort.\n\nTopic: Design, Engineering Tracks, Front-End Desig
 n\n\nSession Chair: Dave Rich (Siemens)
END:VEVENT
END:VCALENDAR