When using formal verification on large DUTs, after solving an initial set of provable assertions, it is common to have some remaining assertions which are not proven -- or disproven -- in the course of the analysis. Even though formal couldn’t conclusively verify the expected behavior, the DUT behaviors recorded up until the analysis halted still provides meaningful information. In this paper, we will show how “Formal Coverage” methodologies and the resulting data enable engineers to effectively judge the quality of verification that these “bounded proofs” provide.
