Presentation
Out of The Box Techniques for Data Path Verification
DescriptionArchitects or designers write C/C++ model to test-out their algorithm at the early stages before design(RTL) is ready or the testbench to test the design is ready. So, verification engineers need to prove the equivalence between the design and golden C/C++ model. The criticality for these equivalence verification of data-path designs (RTL) with their reference high-level C/C++ models, is well accepted. Simulation approaches likes DPI or score boarding can achieve verification completeness to some extent. The means of verifying this equivalence is shifting from simulation to formal gradually, thanks to new solver capabilities available in formal tools and the exhaustive nature of formal.
However complex algorithms often run into the challenge of compiling i.e. building formal model from C++ of in reasonable time. Also, we often struggle to achieve proof convergence on the equivalence check targets, even if we manage to compile the C++ models. While formal methods can be potentially effective, the right methodology is required to overcome these challenges and scale to larger and complex designs. In this paper, we propose several generic techniques that have helped us to generate formal model for complex image processing algorithm like FFT and Decompression units in couple of mins and converge on the properties which was impossible to achieve out of the box. In this process we also uncovered bugs that the traditional verification methods could not catch. All these techniques are reusable, and this paper talks about details on these techniques by taking FFT and Decompression algorithm as an example.
However complex algorithms often run into the challenge of compiling i.e. building formal model from C++ of in reasonable time. Also, we often struggle to achieve proof convergence on the equivalence check targets, even if we manage to compile the C++ models. While formal methods can be potentially effective, the right methodology is required to overcome these challenges and scale to larger and complex designs. In this paper, we propose several generic techniques that have helped us to generate formal model for complex image processing algorithm like FFT and Decompression units in couple of mins and converge on the properties which was impossible to achieve out of the box. In this process we also uncovered bugs that the traditional verification methods could not catch. All these techniques are reusable, and this paper talks about details on these techniques by taking FFT and Decompression algorithm as an example.
Event Type
Networking
Work-in-Progress Poster
TimeMonday, June 236:00pm - 7:00pm PDT
LocationLevel 2 Lobby