Webinar: HLV – Formal Verification of Synthesizable C++/SystemC Designs

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

REGISTER HERE