Formally Verifying SystemC/C++ Designs

We’re seeing an increase in the number of designs employing SystemC/C++. This isn’t surprising given the fact that specific use models have emerged to drive common design flows across engineering teams leading to the adoption of high-level synthesis (HLS) at many large semiconductor and electronic systems companies. These HLS tools are a popular method to rapidly generate design components with varying microarchitectures, while optimizing algorithm processing datapaths rapidly and effectively.

However, the verification of SystemC/C++ designs is largely performed by compiling the design representation using a standard software compiler and debugging the code in a similar fashion to software designs. The IEEE 1666-2011 standard provides a more RTL-simulation-like user experience, but the verification of SystemC code remains a complex and arduous task. Debug, runtime performance, and test complexity are significant hurdles that need to be overcome.

As the level of abstraction increases, so too must the level of verification. At the pre-HLS algorithmic level, verifying the design directly against its specification with less concern for coding detail is a requirement. Functional specifications may be represented easily with assertions and, as such, the use of formal techniques, which allow assertions to be rigorously tested against the design, is a natural choice. New, control-intensive algorithms, now being coded in SystemC, are particularly hard to verify using just simulation.

There are a broad range of formal techniques that can be applied to SystemC design, but OneSpin a Siemens Business has the only automated solution on the market. The product provides a range of automated structural, safety, and activation checks that can be applied without the need for manual assertion creation. Fully functional assertion-based formal verification tools allow for comprehensive assertions to be tested against SystemC/C++ design code. Multiple proof engines can leverage a range of standard and proprietary algorithms to provide in-depth code analysis. The automated solution can also be leveraged on SystemC/C++ hardware design code to help eliminate bugs as early in the design process as possible – saving many engineering hours downstream.

One of our larger customers designing in SystemC was able to use the solution to save significant verification time, vastly improve code quality prior to HLS, avoid unproductive simulation runs and testbench errors, and find corner-case bugs that simulation missed. The advanced multimedia company deployed the solution as a complement to high-level synthesis. This enabled precise diagnostic and direction to improve code, faster runtime and iteration loop, exhaustive formal checking all resulting in better overall SystemC verification.

Formal techniques are well established as a key part of functional verification for hardware designs. Many designers have moved to SystemC/C++ to raise the abstraction level and take advantage of high-level synthesis. The move speeds up hardware design time, but for a corresponding reduction in verification time, the focus must be on the SystemC/C++ source code and not the post-HLS RTL design. The OneSpin SystemC/C++ solution satisfies this need, providing both automated design inspection and full assertion-based verification for high-level designs. HLS users can take advantage full advantage of the most advanced formal verification methods. You can read more about how formal verification is applied to SystemC/C++ design in our white paper “OneSpin Formal Solutions for SystemC/C++ Verification” at https://www.onespin.com/resources/white-papers. You can also get more detail into the case study mentioned above at https://www.onespin.com/customer-stories.