Enhanced Formal Verification Flow for Circuits Integrating Debugging and Coverage Analysis

In this chapter the authors briefly review techniques used in formal hardware verification. An advanced flow emerges from integrating two major methodological improvements: debugging support and coverage analysis. The verification engineer can locate the source of a failure with an automatic debugging support. Components are identified which explain the discrepancy between the property and the circuit behavior. This method is complemented by an approach to analyze functional coverage of the proven Bounded Model Checking (BMC) properties. The approach automatically determines whether the property set is complete or not. In the latter case coverage gaps are returned. Both techniques are integrated in an enhanced verification flow. A running example demonstrates the resulting advantages.