The lights in the Tunnel: Coverage Analysis for Formal Verification

ABSTRACT As formal verification engineers, the authors always face challenges to know the current status of test benches. Many questions need to be answered at certain stages of a project. E.g., do we need more assertions? Did you over-constrain inputs that drop an important design scenario? Are proof bounds for bounded proofs good enough to catch potential design bugs? For the properties that are fully proven, do they cover the design logic that were intended to cover? These four most-asked questions don’t have answers without extracting information from formal engines, which is not feasible for general users. However, like coverages from simulation-based verification, formal verification coverages can be defined and used as matrices to measure formal verification progress and completeness. In this paper, the authors will introduce formal verification coverage models and their usages by real-life examples. The four most-asked questions finally have reasonable and acceptable answers supported by matrices.