Unreachable coverage elimination

Late in a project, simulation coverage reports typically show a long tail of items never hit: lines, branches, FSM transitions, covergroup bins. Engineers spend weeks writing tests for them — sometimes for items that are impossible to reach in the first place.

Formal can answer the question directly. Every coverage item is turned into a cover property; formal either produces a trace (so a test is possible — and the trace shows how), or proves the item unreachable, so it can be excluded with a justification.

Example

Recall phase_seq from lesson 2.2. Its default branch handles both state C and the unused encoding 3. Code coverage may report the condition "phase == 3 in the default branch" as never hit. One cover settles it:

// UCE check for phase_seq: is encoding 3 reachable at all?
c_phase3: cover property (@(posedge clk) disable iff (rst) phase == 2'd3);
// Result: UNREACHABLE  -> exclude the item, citing this proof