Formally identify flaws, ambiguities, and unwanted design difficulties, as well as user restrictions concerns, early in the HLS design and verification process. Despite differences in language, time, and interfaces, Catapult Formal Verification Tools enable verification and coverage closure flow at the C-level.
HL-centric programs are plug-ins compatible with current RTL processes and UVM concepts, having the following goals in mind:
- Examine the design for undefined behaviors.
- Complete the coverage.
- Identify setup errors that alter design behavior.
- Verify the implementation’s accuracy.
- With bug hunting, you may detect discrepancies.
Find Coverage Issues Before Synthesis Efficiently
- Ignore inaccessible coverage points for correct coverage metrics;
- Observe attainable coverage points for simulation replay and improved insight
- Catapult Coverage with industry-standard UCDB database integration
Detect mistakes and setup constraints problems early
- Formally examine memory configuration
- Formally verify that there is enough FIFO depth/size between blocks.
Check implementation and detect differences early
- Early detection of Catapult inferred errors and limitations issues
- Formally validate sequential behavior while maintaining design behaviour/purpose
Find behavior differences early
Formally look for discrepancies between the HLS model, the HLS configuration, and the RTL that was built. Reduces the time and effort required to gain assurance that the desired functionality is preserved without the need for intensive simulation. Mismatches are officially demonstrated and counter-examples are provided.
