Formal verification of synthesizable C++/SystemC designs
Integrate your multi-domain digital thread with a comprehensive enterprise BOM approach
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