R.: Enhanced formal verification flow for circuits integrating debugging and coverage analysis

Abstract: In this paper we briefly review techniques used in formal hardware ver-ification. 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. Compo-nents are identified which explain the discrepancy between the property and the cir-cuit 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 lat-ter case coverage gaps are returned. Both techniques are integrated in an enhanced verification flow. A running example demonstrates the resulting advantages