High-Level Static and Formal Verification
Sequential Formal Verification techniques can be applied to C-source written for HLS. A C-Level verification suite includes simulation, coverage metrics, and formal analysis very similar to direct RTL design flows. Assertions, covers and reachability analysis from C-based formal analysis all combine to give the designer and verifier feedback to close coverage and functionality efficiently.
-
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.