Formal for Coverage Closure

Near the end of a project, the simulation coverage report always has holes: coverage points that no test has hit. For each one, the team must decide whether to write a new test or to exclude the point as impossible. Guessing wastes weeks either way. Formal answers the question exactly: it either produces a trace that reaches the point, which becomes the recipe for a test, or it proves that the point can never be reached. This article classifies four coverage holes of a state machine.

8 min read | Intermediate

What You'll Learn

• Explain how formal helps close simulation coverage
• Turn a coverage point into a cover property or a meant-to-fail check
• Classify holes as reachable, with a trace, or unreachable, with a proof
• Use the classification to write tests and exclusions

The Coverage Problem

Functional coverage in a UVM testbench lists situations that must be exercised: states, transitions, combinations of inputs and states. A typical report at 95 percent coverage leaves hundreds of holes. Some are hard to hit with random stimulus; some can never be hit at all. Without knowing which is which, engineers spend days tuning constraints for points that are impossible.

Formal classifies each hole:

• Reachable: the tool returns a trace. Its input sequence shows exactly how to reach the point, and becomes a directed test or a constraint change.
• Unreachable: the tool proves the point can never happen. It is excluded from coverage, with the proof as justification.

Commercial tools offer this as an unreachability app that reads the coverage database directly. By hand, each hole becomes a cover property.

The Example: Four Holes

The request controller from the finite state machines article, in its fixed form, has these four holes in a simulation coverage report:

As covers in SVA:

c_ack:  cover property (@(posedge clk) disable iff (rst) busy && ack);
c_req:  cover property (@(posedge clk) disable iff (rst) err && req);
c_both: cover property (@(posedge clk) disable iff (rst) busy && err);
c_tmr:  cover property (@(posedge clk) disable iff (rst) state == ERR && t != 3'd0);

Results

In the lab form, each cover is a meant-to-fail assertion, such as always @(*) if (!init) assert (!(busy && ack));. On the lab engine:

• Acknowledge while waiting: fails at step 2, so reachable. The trace: a request in step 1, the controller waits in step 2, and the acknowledge arrives in that same cycle. A test only needs an acknowledge one cycle after a request; a random test whose memory model always takes two cycles or more never produces it.
• Request while in ERR: fails at step 6, so reachable: a request, four cycles without an acknowledge, and another request while in ERR.
• Busy and error together: passes. In prove mode, with k-induction and with PDR, it is proven: busy and err decode different states, so they can never be high together.
• ERR with the timer running: passes, and is proven as well: the controller clears the timer whenever it enters ERR.

The first two become directed tests, written from the traces. The last two are excluded from coverage, each with a short note citing the proof. The coverage report is then complete, honestly.

Reading a Cover Trace as a Test

A cover trace lists the inputs in every cycle, which is a test stimulus. For "acknowledge while waiting": reset in step 0, req in step 1, ack in step 2. In a UVM testbench, that becomes a sequence that issues a request and configures the memory model to answer after one cycle. Many teams convert cover traces into tests automatically.

Running It in ChipVerify Lab

The example below is the fixed controller with the four coverage points as meant-to-fail checks, of which only the first is active. Run it, then activate the others one at a time.

Common Mistakes