Formal verification of synthesizable C++/SystemC designs

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. Siemens offers several apps to verify and clean C++ HLS code before running HLS and then check the equivalency between C++ and RTL.

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