Formal Verification of Synthesizable C++/SystemC Designs

High-level synthesis (HLS) is a design flow in which design intent is described at a higher level of abstraction than RTL, such as in SystemC/C++ or MATLAB. HLS tools are expected to synthesize this code to RTL which can be input to the traditional RTL downstream flow (RTL / GDS).

Formally checking generated RTL can be difficult to analyze as errors cannot be correlated to the HLS source code. Questa™ HLV can help overcome this challenge with high-level verification (HLV). Siemens offers several apps to verify and clean C++ HLS code before running HLS and then check the equivalency between C++ and RTL to guarantee that the golden C++ is equivalent to the final RTL design.

What you will learn

• Where to apply HLV tools for C++/SystemC designs
• How to run HLV tools
• How to verify C++ designs before running HLS (clean the code)
• How to prove equivalency between C++ and generated (or manually written) RTL
• Methodologies for applying HLV equivalence checking

Overview of HLV tools and Capabilities

Designing accelerators in C++/SystemC provide huge benefits. HLS delivers a large return of investment in key verticals: image sensor processing, video compression, AR/VR, custom AI/ML inferencing, 5G/modem/Wifi, optical communications, embedded SoC acceleration, and faster design time and architectural exploration — all with orders of magnitude speedup in simulation.

Adoption of HLS creates a new verification challenge

• How do I know if my C++/SystemC is clean and synthesizable?
• How do I know if my C++/SystemC is correct?
• Did the synthesis tool give me what I wanted?
• How do I integrate, cover, and debug the RTL generated from HLS?

Siemens Questa 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 apps include: formal autochecks for fully push-button analysis of the HLS design, a variety of formal-based apps, SystemVerilog Assertions (SVA) based formal verification support, comprehensive simulation coverage metrics, and HLS code versus RTL equivalence checking.