Something new in High Level Synthesis and High Level Verification

As SoC complexities continue to expand to billions of transistors, the quest for higher levels of design automation also rises. This has led to the adoption of High-Level Synthesis (HLS), using design languages such as C++ and SystemC, which is more productive than traditional RTL design entry methods. In the RTL approach there are formal tools for source code coverage reachability analysis and assertion verification, yet those two formal tools were missing from HLS tool flows, until now. I spoke with David Aerne, Principal Technologist, Catapult Division, Siemens EDA to get an update on their newest HLS and High-Level Verification (HLV) capabilities.

David initially outlined the scope of tools that comprise HLV, with design checking to look for synthesizable code, and static linting with deep formal methods to ensure correctness. For design verification the focus is on functional correctness by using automatic formal property checking of HLS source code along with metrics driven dynamic verification.

These HLV concepts map into two new apps within the Catapult High-Level Verification Flow:  Catapult Formal Assert and Catapult Formal CoverCheck.

Catapult Formal Assert

The idea here is to formally prove assertions for function verification by testing design assumptions that are too hard to simulate, and to validate C++ and SystemC for valid ranges, traps and even dead code. Engineers can use assert, assume and cover, while the counter-examples create a C-level testbench.

Catapult Formal CoverCheck

After Catapult Coverage has been enabled during dynamic simulations of your HLS design, you decide if the coverage metrics have been met, and when you need higher coverage, then the Catapult Formal CoverCheck app comes into use. The CoverCheck push-button app formally analyzes coverage holes to bin coverage items into one of three possible categories: reachable, unreachable and undecided with the results predominately being either reachable or unreachable results. Both waivers and counter-examples are produced by CoverCheck. All of the coverage information, including the waivers, are compatible with the Siemens EDA Unified Coverage DataBase (UCDB) which provides the foundation for the Verification Management capabilities integrated within the Catapult HLV flow.

Summary

Designing with C++ and SystemC is more productive than using traditional RTL methods, and now HLV has become even more productive by adding formal property checking and coverage reachability analysis. Siemens EDA has been in the HLS and HLV business for over two decades now, so they have plenty of experience, and adding more apps to HLV just makes the flow more attractive to design and verification engineers.

Verifying at the high-level promises a 100X improvement over RTL methods. Metrics-driven HLV is now possible by using formals methods and coverage analytics, so that your team knows that their design meets the targets. Industries that require Functional Safety (FuSa) and that are following standards like DO-254  and ISO 26262 will certainly benefit from these new HLV apps.

Learn more about Catapult Formal Verification tools online.

Related Blogs

• New Tool that Synthesizes Python to RTL for AI Neural Network Code
• Emerging Stronger from the Downturn
• An Update on HLS and HLV
• Pushing Acceleration to the Edge
• A Fresh Look at HLS Value
• HLS in a Stanford Edge ML Accelerator Design
• DARPA Toolbox Initiative Boosts Design Productivity