Catapult Formal Verification

Overview

Catapult Formal Verification Tools

Formally find mistakes, ambiguities and undesirable design issues, user constraints problems early in the HLS design and verification process. Even with differences in language, timing, and interfaces, Catapult Formal Verification Tools enable verification and coverage closure flow at C-level.

Catapult Formal Verification Apps
KEY FEATURES

Catapult Formal Verification Tools

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

C-LEVEL COVERAGE CLOSURE

Find Coverage Issues Before Synthesis Efficiently

• 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

SMART SETUP CHECKING

Detect mistakes and setup constraints problems early

  • Formally check memory setup

  • Formally check for sufficient FIFO depth/size between blocks

Catapult Formal Smart Setup Checking

CORRECTNESS WITH CONFIDENCE

Check implementation and detect differences early

  • 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.

CATCH BUGS EARLY

Find behavior differences early

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.

Ready to discuss Catapult Formal Verification Tools?

Any questions you may have, we will have the answers!

Email us at hls-hlv.sisw@siemens.com

image of arrows

Join the IC Design Community

Join the discussion on new topics, features, content, and technical experts.

two squares on top of each other

Catapult Support

Access detailed documentation, on-demand training resources and more.

Consulting Services Icon

EDA Consulting

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