Presentation
Enhancing Quality and Reducing Verification Effort for RTL Implementations against High-Level C/C++ Models using Formal Equivalence
SessionAdvanced Verification
DescriptionThe complexity of modern System on Chip (SoC) designs has led to advanced verification techniques, facing the challenge of detecting undetected functional failures.
In the area of wireless and wireline communication products, designers initially model Digital Signal Processing (DSP) blocks 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 Verification Methodology (UVM) dynamic simulations, yet subtle bugs in critical DSP blocks can remain hidden.
To address this, Formal Equivalence Verification (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 coverage of the design state space.
This paper presents an in-depth exploration of complex FSM with Datapath verification, namely Floating-Point MAC, Tone Generator, and Automatic Gain Control, utilizing Formal Equivalence methodology. Despite these DSP blocks had been validated throughout UVM dynamic simulations which lasted months, subtle corner cases hidden bugs were spotted in few weeks by adopting the proposed flow, therefore reducing the verification effort.
In the area of wireless and wireline communication products, designers initially model Digital Signal Processing (DSP) blocks 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 Verification Methodology (UVM) dynamic simulations, yet subtle bugs in critical DSP blocks can remain hidden.
To address this, Formal Equivalence Verification (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 coverage of the design state space.
This paper presents an in-depth exploration of complex FSM with Datapath verification, namely Floating-Point MAC, Tone Generator, and Automatic Gain Control, utilizing Formal Equivalence methodology. Despite these DSP blocks had been validated throughout UVM dynamic simulations which lasted months, subtle corner cases hidden bugs were spotted in few weeks by adopting the proposed flow, therefore reducing the verification effort.
Event Type
Front-End Design
TimeTuesday, June 252:00pm - 2:15pm PDT
Location2010, 2nd Floor
Design
Engineering Tracks
Front-End Design