Read on for the complete answer…
Gone are the days when formal verification was not equipped with code coverage. We have come a long way in integrating code coverage as a standard feature of formal verification.
The general purpose of code coverage remains the same, i.e., find the reachability holes in the design, which arise from a lack of input stimulus and from deadcode. However, the root-cause of insufficient input stimulus is different in formal verification vs. simulation. In simulation, code coverage holes are indicative of insufficient quality and quantity of tests, whereas imperfect code coverage in formal points toward a presence of over-constraints in the setup or insufficient runtime of the formal proof.
The aforementioned difference between formal and simulation is primarily because of the fact that simulation uses a zero-plus (0+) approach and formal uses an infinity-minus (∞-) approach. In simulation, we start from zero coverage and we add tests to provide input stimulus that exercises different pieces of code and improves code coverage over time. However, theoretically, we start from infinite input stimulus (legal as well as illegal) in formal. With enough runtime, formal tools will end up covering all the code. It is when we run the checkers that formal tools will throw false counterexamples at us and we then need to add appropriate constraints to disallow illegal stimulus. Adding constraints may lead to a reduction in code coverage.