HLV: Formal Verification of Synthesizable C++/SystemC Designs and Prove Equivalency with RTL Code
Formal check tools are difficult to be analyzed on generated RTL (as the errors cannot be correlated to HLS source code) Catapult Formal/Onespin SystemC help to overcome this challenge. Under HLV there are several apps, to verify and clean C++ HLS code before running HL Synthesis and then apply equivalency between C++ and RTL to guarantee that golden C++ is equivalent with final RTL design. In this webinar you will learn how to apply HVL tools for C++/SystemC designs.
-
Session Registration
-
Session Overview
High-Level Synthesis (HLS) is design flow in which design intent is described at a higher level of abstraction such as SystemC/C++/Matlab/etc. HLS tools are expected to synthesize this code to RTL which can be input to the traditional RTL downstream flow (RTL/GDS).
Formal check tools are difficult to be analyzed on generated RTL (as the errors cannot be correlated to HLS source code) Catapult Formal/Onespin SystemC help to overcome this challenge. Under HLV there are several apps, to verify and clean C++ HLS code before running HL Synthesis and then apply equivalency between C++ and RTL to guarantee that golden C++ is equivalent with final RTL design.
Under HLV there are 7 apps:
- Catapult C Design Checker
- Catapult Formal Assert
- Catapult CoverCheck
- Catapult Formal SLEC
- SLEC System
- OneSpin SystemC Inspect
- C Coverage
Siemens HLV tool offerings offer early bug detection immediately after the HLS code is written, including exhaustive formal analysis, comprehensive simulation-based coverage metrics, allowing faster runtime and iteration loops. These are: Formal autochecks for fully pushbutton formula analysis of the HLS design, a variety of formal-based apps, SVA assertion-based formal verification support, comprehensive simulation coverage metrics, and HLS code to RTL equivalence checking.
What You Will Learn
- How to apply HLV tools for C++/SystemC designs
- How to run Siemens HLV tools
- How to verify C++ designs before running HLS (clean the code)
- Prove equivalency between C++ and generated (or manually written) RTL
- Methodologies to apply HLV equivalence checking
Who Should Attend
- Verification engineers that verify HLS designs (Catapult and other HLS tools)
- Engineers that verify equivalence of C++ vs RTL
- Design & Verification Engineers & Managers
Products Covered
- Catapult Formal, SLEC System and OneSpin SystemC Inspect
