Funtional Verification (vs) Formal Verification .!

SystemVerilog
, , , ,
1

Hello All,
why Formal Verification is needed? In Functional verification, all functionality mentioned in the specification is verified. we hitting 100% code coverage and 100% functional coverage. but still, we moving formal verification.!!! why is that so important? Are there any criteria that say this functionality should be verified with formal verification?

2

In reply to Malai_21:
we hitting 100% code coverage and 100% functional coverage.

  • 100% code coverage, that does not necessarily translate to meeting design requirements, far from it.
  • 100% functional coverage Wow, 100%! are you sure? Have you covered all the possible paths and sequences with functional coverage? I seriously doubt it.

7.1.1 What is formal property verification ?
Formal property verification (FPV) is verification process in which analysis of a design with mathematical techniques yields a logical inference about whether the properties (specified in an assertion language. like SVA) hold for all legal behavior of the design. If a property is declared true by a formal verification tool, no simulation can show it to be false. However, if a property does not hold for all legal scenarios, then the formal verification process provides a specific counterexample to the property (i.e., show a sequence example that demonstrates a failure case).
Formal verification is in contrast to simulation-based methodologies that rely on the application of test vectors, and on the observation of results as compared to expected behavior. That observation is typically performed with a verifier model that understands the protocols, transactions, and expected results. FPV works in almost the opposite fashion: it tries to “break” the system (or violate the expectations) by applying as many possible legal input combinations, as constrained by the assume statements and/or other constraints. While this approach sounds great, it has its own set of issues: the necessity to eliminate illegal input combinations, and the need to specify the “expected behavior” in a formal manner that can be interpreted by the tools.
7.1.2 Why formal property verification
Formal property verification of digital designs is very useful for the many reasons; below are tidbits and notes about formal verification.

  1. Formal property verification offers quick verification of design iterations, without a testbench, to arrive at a working model. This enables the designers to validate their designs at the block-level. Verification engineers can focus on specifying the design properties and creating larger level simulation-based verification environments (e.g., for cluster, full chip, system level). The block-level assertions can also be reused at higher levels as additional checkers/monitors.
  2. Candidate designs ideal for formal verification include those with focus on control and tricky areas of the design. Long sequences and data analysis with local variables are best served with simulation.
  3. Formal analysis is complete, covers complex test sequences, and provides counterexamples that demonstrate functional errors. A review of the failed properties that define the requirements, and an analysis of the counterexample waveforms help in identifying the sources of errors. Those errors can be RTL errors, misuse of SystemVerilog, misunderstanding of the requirements, or property specification errors. In any case, the engineer is challenged to fully understand the design and the requirements.
  4. Corrections of these errors can be verified with another run of the formal verification tools. This methodology is analogous to the edit/compilation/synthesis process used in RTL design and synthesis to eliminate early mortality (or gross errors) in the design.
  5. Most vendors incorporate automatic static checks into their formal verification tools. The checks will catch such things as unreachable code, deadlocks, and constant nets. No user provided assertions are needed, though assumptions provided can be used to prevent false negatives.
  6. Formal verification coverage analysis capability helps in ensuring that no design behavior is missed during verification. Coverage analysis uncovers holes in the verification plan, detects unverified design functionality, and finds errors and omissions in design specifications. It generates diagnosis information guiding the user in writing additional assertions to close verification holes.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: