Resolve coverage holes with tests, proofs and exclusions

How-to Last tested 25 October 2026

An unhit coverage point needs a reason, not just more random seeds. First check whether the stimulus can produce its activation, then use a directed test, a scoped formal proof or a written configuration exclusion as appropriate. In this example, 32 seeds miss a legal long transfer, a directed case reaches it, and a separate one-step proof shows the full-and-empty expression is a combinational contradiction for any two-state occupancy.

Give each point a requirement and a disposition

The original packet gate admits a nonzero-length request when it is not full. It has two occupancy flags and an optional debug admission signal. The example tests a build with DEBUG=0. These choices create three different reasons a counter can stay zero: the driver never generates a length of fifteen, the two occupancy flags cannot be true together, and the debug feature is disabled in this build.

Those reasons are not interchangeable. The long-transfer goal is a legal behavior that the initial stimulus fails to exercise. The contradictory-flags counter observes a forbidden condition associated with the mutual-exclusion requirement, so a hit would be a bug rather than progress toward a target percentage. The debug counter belongs to another configuration. A single aggregate “uncovered” count would erase the action each one needs.

Keep the meaning of the goal beside its identifier. A positive functional goal asks that useful behavior occur. A forbidden-state observation asks whether a violation occurs; absence of simulation hits alone does not prove absence of the violation. A configuration exclusion is a declared scope decision, not an empirical result. This distinction also prevents a negative requirement from being mistakenly counted as a bin that must be hit.

Run the original gate and reproducible stimulus

The design and testbench are separate complete files. Save both in a working directory and use the exact commands for Icarus 13.0 and Verilator 5.052. The code below is the same code those runs consumed, including the explicit width conversions and generator constants.

// SPDX-License-Identifier: MIT
module packet_gate #(parameter DEBUG = 0)(
  input clk, reset, request, release_slot, debug_request,
  input [3:0] length,
  output accepted, debug_accepted, full, empty, impossible,
  output [1:0] occupancy
);
  reg [1:0] used = 0;
  assign full = used == 3;
  assign empty = used == 0;
  assign impossible = full && empty;
  assign occupancy = used;
  assign accepted = request && !full && length != 0;
  assign debug_accepted = DEBUG && debug_request && accepted;
  always @(posedge clk) begin
    if (reset) used <= 0;
    else if (accepted && !release_slot) used <= used + 1'b1;
    else if (release_slot && !empty && !accepted) used <= used - 1'b1;
  end
endmodule

// SPDX-License-Identifier: MIT
`timescale 1ns/1ps
module tb;
  reg clk = 0, reset = 1, request = 0;
  reg release_slot = 1, debug_request = 1;
  reg [3:0] length = 0;
  wire accepted, debug_accepted, full, empty, impossible;
  wire [1:0] occupancy;
  reg [31:0] state;
  integer seed = 1, directed = 0;
  integer short_seen = 0, long_seen = 0;
  integer impossible_seen = 0, debug_seen = 0, checked = 0;
  packet_gate dut(clk, reset, request, release_slot, debug_request,
                  length, accepted, debug_accepted, full, empty,
                  impossible, occupancy);
  always #5 clk = !clk;
  task observe;
    #1;
    if (accepted && length <= 7) short_seen = short_seen + 1;
    if (accepted && length == 15) long_seen = long_seen + 1;
    if (impossible) impossible_seen = impossible_seen + 1;
    if (debug_accepted) debug_seen = debug_seen + 1;
    if (!accepted) $fatal(1, "expected admission in empty simultaneous-release setup");
    checked = checked + 1;
    @(posedge clk);
  endtask
  initial begin
    if ($value$plusargs("seed=%d", seed)) begin end
    if ($value$plusargs("directed=%d", directed)) begin end
    state = 32'(seed);
    @(negedge clk);
    reset = 0;
    request = 1;
    for (integer i = 0; i < 16; i = i + 1) begin
      state = 32'd1664525 * state + 32'd1013904223;
      length = 4'(1 + state % 7);
      observe();
      @(negedge clk);
    end
    if (directed) begin
      length = 15;
      observe();
    end
    $display("seed=%0d directed=%0d checked=%0d short=%0d long=%0d impossible=%0d debug=%0d",
             seed, directed, checked, short_seen, long_seen,
             impossible_seen, debug_seen);
    $finish;
  end
endmodule

The driver uses a defined 32-bit linear congruential generator so that the seed-to-length mapping is visible in the source rather than dependent on a simulator’s random-number implementation. After each update, it maps the value to a length from one through seven. That bias is intentional and decisive: no number of these seeds can generate fifteen. Calling the run “random” does not broaden the range produced by its constraint.

The test holds release active while issuing requests, keeping the setup free of accumulating occupancy. It checks that every requested ordinary transfer is admitted in that setup, then counts the observed requirement conditions. It does not exercise queue filling, overflow rejection or drain ordering. Those are worthwhile additional scenarios, but their existence must not be inferred from a run whose stimulus intentionally avoids them.

The Verilator build retained warnings about the design module lacking the testbench’s time-scale declaration and the integer directed flag used as a condition. The build used the recorded nonfatal-warning option and completed; the literal messages remain with the run. No warning-free compilation or broader language-conformance claim is made.

Merge evidence without counting repeated work twice

The recorded seed list is one through 32, with 16 transfers per seed. Each simulator therefore observes 512 admitted short transfers, zero long transfers, zero contradictory-flag observations and zero debug admissions. The per-seed and merged results retain every seed’s counts. They are original functional counters printed by the testbench, not native covergroup, line, branch or toggle reports.

Both simulators produced the same counters for this stimulus. That agreement supports reproducibility of this particular digital example; it is not an accuracy ranking or proof that the two tools will agree on every language construct. The simulator observation dataset discusses versioned behavior under other inputs and configurations without merging these new runs into that existing dataset.

For a functional hit goal, merging should usually retain both total observations and whether the goal was reached at least once. Ten copies of the same seed can increase the count without adding a new tested condition. Preserve the seed, generator, configuration and source hash so that a large count remains traceable to actual stimulus. Do not merge differently configured builds merely because their counters use the same names.

The directed run uses seed one for the initial 16 short transfers, then supplies length fifteen once. It reports 17 checked admissions, 16 short hits and one long hit. Its repeated short sequence is visible rather than silently treated as new diversity. Combined totals would be 528 short hits and one long hit per simulator, but the useful coverage change is the new long-transfer observation, not the larger total.

Close the reachable hole with the smallest directed case

The directed case changes the activation that the seeded driver could not produce: it assigns fifteen directly before calling the same observation task. The gate admits the transfer in the empty, simultaneous-release setup, and the long counter increments. There is no need to redesign the generator to demonstrate this missing case. The common checker and observation timing make the added evidence easy to compare with the original sequence.

Closing this one point does not validate every long-packet behavior. The gate models admission using a length field; it does not transmit fifteen data beats or check their contents. A real packet implementation would need payload, termination, backpressure and error scenarios linked to its contract. State what the point observes: here it is the admission of a request carrying length fifteen.

If a directed input still failed to hit the point, inspect the checker and observation before escalating the seed count. A trigger can be present in the stimulus but disappear through configuration, selection, reset or backpressure. The coverage counterexample demonstrates the complementary problem: every reported code point can execute while a required situation never activates the checker at all.

Prove the forbidden-state condition at its actual scope

The expression impossible = full && empty is a combinational contradiction: the same two-bit value cannot equal three and zero. This does not depend on the set of reachable states. The additional contradiction_any_state.ys query removes the register’s initialization constraint and proves the expression zero in one arbitrary state in a two-state model. The corrected induction command below also succeeds, with -seq 1 removed so its base check includes the declared initial state; induction is unnecessary for this expression.

# SPDX-License-Identifier: MIT
read_verilog -formal -sv design.sv
prep -top packet_gate
sat -tempinduct -maxsteps 1 -prove impossible 0 -show-ports

The result is consistent with the definitions: full means the two-bit occupancy equals three, while empty means that same value equals zero. A single two-state value cannot satisfy both equalities. The Yosys record preserves both proof commands, their input hashes and results. The arbitrary-state check is a one-step combinational argument, not evidence that a difficult sequential state is unreachable. Its first command variant using -set-init-def alone returned an internal assertion before proving anything; the recorded successful query removes that option and leaves the initial state unconstrained in the default two-state model. The solver did not establish an arbitrary implementation’s flag correctness; it established this specific expression in this specific model¹.

Do not translate that digital proof into a statement about analog transitions or clock-domain behavior. Unknown values, metastability and independently synchronized flag signals require different modeling and checks. If the implementation later computes the two flags through separate pipelines or clock domains, this argument no longer describes the changed circuit. The proof must follow the source and assumptions, not just the requirement’s familiar name.

Write the exclusion before adjusting the denominator

The debug disposition is: “R4 applies only when DEBUG=1; this run elaborates DEBUG=0, which forces debug admission low. Exclude R4 from this configuration’s positive functional goals. Re-enable and test it in any debug-enabled release.” That rationale names the requirement, parameter value, reason and condition that invalidates the exclusion. It does not assert that the enabled feature was tested.

Keep that record with the coverage plan and configuration rather than burying it in a reporting command. A later build that enables debug should reopen the obligation even if all the ordinary transfer counters remain unchanged. A proved contradictory expression and a configuration exclusion should also remain separate entries: the former is a property of this model, while the latter states which build this test is intended to cover.

For a handoff, deliver the seed list, individual outputs, merge rule, directed result, proof command and exclusion rationale together. The formal-results guide explains why bounded success, a witness and completed induction make different claims. A useful completion record lets another engineer reconstruct those claims without guessing what an impressive percentage left out.

Not covered on this page

• Native covergroups or line, branch and toggle coverage percentages.
• Packet payloads, queue-fill stress or exhaustive transaction ordering.
• Debug-enabled behavior, analog flag transitions or clock-domain safety.
• Verification closure for a production design.