Ensure Equivalence Of Synthesizable C++/SystemC Designs Against Generated/Handwritten 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 One HLV can help overcome this challenge with high-level verification (HLV). Siemens offers several apps to check the equivalency between C++ and generated/hand-written RTL to guarantee that the golden C++ is equivalent to the RTL design.

This article introduces you to some of the fundamentals of applying HLV verification: where to apply HLV tools for C++/SystemC designs, how to prove equivalency between C++ and generated (or manually written) RTL, and methodologies for applying HLV equivalence checking.

How equivalence tools help

Along with its many benefits, adoption of HLS creates a new verification challenge, such as: how do I know if my C++/SystemC is clean and synthesizable? How do I know if my optimized C++/SystemC is correct? Did the synthesis tool give me what I wanted?

This is where HLV tools can help you out. Questa One HLV has two tools for equivalence verification: Catapult Formal SLEC and SLEC System. Both allow you to verify that your SystemC/C++ design is 100% equivalent to the RTL.

Fig. 1: The Questa One HLV flow.

Catapult Formal SLEC

Catapult Formal SLEC compares C++ to the RTL generated from that same source by Catapult HLS. It is a push-button solution with automated set up. The Catapult Formal SLEC test confirms the functional correctness of the RTL against the C++.

Formal verification must assume that the reference/spec model is fully correct, therefore HLV of the C++ is preferred to occur before CFSLEC. With Catapult Formal SLEC, using formal verification assures that the synthesis process step to transform C++ to RTL did not alter the logic or computations/resolutions/truncations that existed in the C++. The Catapult Formal SLEC flow automatically adjusts and builds a verification setup that makes the process of mapping the reference model to the implementation effortless.

Fig. 2: Catapult Formal SLEC flow.

SLEC System

In the case of specification verification when handwritten RTL is the implementation model, SLEC System compares the C++ to the handwritten RTL. Formal proofing will fully cover all input numerical possibilities and is appropriate for datapath processing checks. Setup allows comparison despite differences in timing, interfaces, and levels of abstraction.

Fig. 3: SLEC system flow.

Also, SLEC System can be used for equivalence checking of SystemC versus an optimized SystemC model. That is often the case with golden SystemC designs and when some optimizations are applied to the golden model, such as power, area, or optimizing data-path calculations.

A third use-case for SLEC System is equivalence checking of the RTL versus optimized RTL. While SLEC System can do the mapping automatically, it is possible to do manual mapping if needed.

More confident design

Formal verification indeed offers numerous advantages for the verification process. Its ability to exhaustively explore all possible states of a design, coupled with its capacity to provide rigorous proofs of equivalence, makes it a valuable tool for ensuring the reliability and correctness of hardware systems.

However, with advancements in solvers, Questa One HLV SLEC tools, and the development of FV-friendly requirements, the applicability of Questa One HLV SLEC in the industry is steadily increasing. Companies are recognizing the importance of incorporating Questa One HLV SLEC into their verification processes to enhance the quality and equivalence of their products.

Overall, Questa One HLV is a powerful platform that, when used effectively, can help companies achieve higher levels of confidence in the correctness of their hardware designs. As the technology continues to evolve and mature, it holds great promise for addressing the verification challenges faced by the industry today and tomorrow.

To learn more, download the paper “Formal Verification of Synthesizable C++/SystemC designs.”