Catapult Formal Verification Tools

Formally find ambiguities and undesirable design issues, and user constraint problems early in the HLS design and verification process. CFormal Apps target specific logic areas with specific preset tests and property checks. CFormal Tools enable verification and coverage closure flow at C-level.

KEY FEATURES

Catapult Formal

HL centric apps are plug-in compatible with existing RTL flows & UVM principles, targeting:

  • Check design for undefined behaviors
  • Achieve coverage closure
  • Detect setup mistakes that change design behavior
  • Check implementation correctness
  • Detect differences with bug hunting

Formal & Static Checks for C++/SystemC

Catapult Design Checker provides multiple pushbutton static and formal checking modes that lessen the need for simulation-based verification of your design. Coding issues, design source ambiguities, QoR concerns, and sources of potential HLS C++/SystemC to RTL mismatches are rapidly caught and feedback is provided as to the source and cause. 

Catapult design checker - Formal & Static Checks for C++/SystemC
  • Waive unreachable coverage points for accurate coverage metrics
  • Witness reachable coverage points for simulation replay, greater insight
  • Plug-play integration with Catapult Coverage with industry standard UCDB database
Efficient Coverage Closure Flow
  • Formally check memory setup
  • Check user-written memory constraints for correctness
Catapult Formal Smart Setup Checking
  • Detect Catapult inferred mistakes and constraints problems early
  • Formally check sequential behavior maintain design behavior / intent
Detect Catapult inferred mistakes and constraints problems early and formally check sequential behavior maintain design behavior / intent.</br>

Formally search for differences between the HLS model the HLS setup and created RTL. Significantly reduces the time and effort to establish confidence that the intended functionality is maintained without requiring exhaustive simulation. Mismatches are formally proven and flagged with counter-examples.

Formally search for differences between the HLS model the HLS setup and created RTL. Significantly reduces the time and effort to establish confidence that the intended functionality is maintained without requiring exhaustive simulation. Mismatches are formally proven and flagged with counter-examples.

Formal Assertion Checks for C++ and SystemC

Catapult Formal Assert is a formal verification app integrated with Catapult HLS. Assertions written in C-Source will be evaluated with powerful formal solvers that provide fast response, configurable timeouts and solve strategies, and a robust debug environment. Assert, assume and cover are supported. Counter-examples create a C-level testbench and default gdb settings as well as a SEDA's Visualizer graphical waveform debugger.

ProdImg CFormalAssert 640x480

Catapult on-demand training

The Catapult High-Level Synthesis (HLS) on-demand training library contains a set of learning paths with modules to introduce engineers to HLS and high-level verification.

High-Level Synthesis and Verification Group

A group to discuss the finer points of design and verification using Siemens EDA HLS and HLV tools. Join the discussion on new topics, features, content and technical experts.

HLSLibs

A free and open set of libraries implemented in standard C++ for bit-accurate hardware and software design. It's an open community for exchange of knowledge and IP for HLS that can be used to accelerate both research and design.

HLS Design and Verification Blog

Blog covering next generation high-level synthesis (HLS) design and verification methodologies and techniques.

Headset

Catapult Support

Access detailed documentation, releases, resources and more.

EDA consulting

Helping you achieve maximum business impact by addressing complex technology and enterprise challenges with a unique blend of development and design experience and methodology expertise.