Most false positives (i.e. missing design bugs) during the practice of model checking on industrial designs can be reduced to the problem of a failing cover. Debugging the root cause of such a failing cover can be a laborious process, when the formal testbench has many constraints. This article describes a solution to minimize the number of model checking runs to isolate a minimal set of constraints necessary for the failure. This helps improve formal verification productivity.
Formal verification in the form of model checking has become an integral part of the chip design sign-off process at many semiconductor companies. The process involves building formal testbenches that can exhaustively verify certain design units.