High-Level Static and Formal Verification
Sequential Logic Equivalence Checking (SLEC) and Formal Verification techniques provide robust validation for High-Level Synthesis (HLS) C-source designs. This comprehensive verification framework integrates advanced formal analysis methods. The C-Level verification suite combines simulation capabilities, coverage metrics, and formal property verification, mirroring established RTL design flows while operating at a higher abstraction level. Through formal proof techniques, designers can leverage assertions, coverage analysis, and reachability studies to validate design behavior systematically. The integration of formal methods with HLS enables automated proof of functional equivalence between high-level specifications and RTL implementations, while property checking ensures comprehensive verification closure. This powerful combination of static analysis and formal verification methodologies helps teams achieve thorough design validation and efficient coverage closure, significantly reducing verification cycles.
-
Overview
High-Level Static and Formal Verification Overview
Verificationacademy.com provides a very good verification technique, education and training site. C-source verification closely tracks RTL-source verification methods for both dynamic coverage and formal verification.
Formal verification uses multiple methods to check the correctness a design. Techniques include:
- Static analysis ranges from fairly simple source code "linting" to more complex checks that require the tool to build and evaluate a model. Checks that focus on correctness of a specific characteristic are often referred to as formal apps.
- Directed Formal Apps focus on proving a specific characteristic about a design and often are push-button or require little user configuration. These tools can check design details such as arithmetic overflow/underflow, floating-point number properties, array access bounds checks, and uninitialized variable usage . Reachability analysis can also find unused or "dead" code that does not need to be exercised by functional verification.
- Formal Assertion Based Verification proves that a design has specific defined properties. Usually, the assertions created for simulation are re-used here as properties that the design must hold. For proving some properties this can be a push-button process, but property verification as a whole can require deep expertise in defining assumptions, selecting the scope of the proof, and understanding counterexamples.
- Formal Equivalence Verification proves that a portion of the design matches a formal (or "reference") model. Due to the advanced transformations done by HLS, equivalence verification may not be a push-button process, and can require formal expertise in scoping the proof and pruning the design to give reasonably sized problems to proof engines.
These formal techniques can be applied with commercial tools to both C-source and RTL-source domains. Productivity of the formal tool user is often a challenge that depends on the complexity and size of the design units being checked. A hybrid approach of test coverage based on both dynamic and formal verification can achieve testing goals with minimal roadblocks and optimal productivity.