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.
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
• 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
SMART SETUP CHECKING
Formally check memory setup
Formally check for sufficient FIFO depth/size between blocks
CORRECTNESS WITH CONFIDENCE
Detect Catapult inferred mistakes and constraints problems early
Formally check sequential behavior maintain design behavior / intent
CATCH BUGS 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.
Email us at email@example.com
Join the discussion on new topics, features, content, and technical experts.
Access detailed documentation, on-demand training resources and more.
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.