Minimizing Constraints to Debug Vacuous Proofs

Most of the design bugs missed during the practice of model checking on industrial designs can be reduced to the problem of a failing cover. When the formal testbench has many constraints, debugging the root cause of such a failing cover can be a laborious process. This article from Mentor Graphics describes a method to minimize the number of model checking runs to identify a minimal failing subset (MFS) of constraints. This solution has increased the productivity by reducing the iterations required to debug vacuous proofs.

Read More