How to avoid the pitfalls of mixing formal and simulation coverage
Coverage as a metric
Simulation-generated code and functional coverage defined
Code coverage is simply the percentage of RTL code measuring the number of statements in a body of code that have been executed through a test run, and which statements have not. While it is important that the testbench can exercise all of the RTL code—i.e., there is no dead code, implying a bug in the DUT, the design can still be missing important functionality and/or the paths to key functions are in violation of the specification.
Functional coverage from RTL simulation is the metric of how much design functionality has been exercised—a/k/a covered by the testbench or verification environment—which is explicitly defined by the verification engineer in the form of a functional coverage model. In its basic form, it is user-defined mapping of each functional feature to be tested to a cover point, and these coverage points have certain conditions (ranges, defined transitions or cross etc.) to fulfill before it is reported as 100% covered during simulation. All these conditions for a cover point are defined in form of bins. A number of cover points can be captured under one covergroup, and a collection of cover groups is usually called a functional coverage model.
During simulation, when certain conditions of a cover point are hit, those bins (conditions) are getting covered and thus it gives a measurement of verification progress. After executing a number of testcases, a graphical report may be generated to analyze the functional coverage report and plans can be made to cover up the holes by creating new tests that will traverse the as-yet unexercised areas of the DUT code.