# Coverage-hole example

Original source and commands: MIT. Original observations: CC BY 4.0. Copy the files into a separate working directory before building. No binaries or third-party libraries are distributed.

Pins: Icarus Verilog 13.0 commit `dfeee909ed9f20b4870dd93423156c0170c0e1ff`; Verilator 5.052 commit `ea338be98e1e838d3518809ce8899f85a009963c`; Yosys 0.70+post binary-reported revision `0c11ea098be065e585a90a06e7b7da49936cf231` (official `v0.70` release-tag commit `28ba3cb926fe376fa05ebfc1b921747d011d4557`). Run records under `/data/measurements/printed-hdl/` contain exact versions, source hashes and literal outputs.

## Exact compile and proof commands

```sh
iverilog -B "$ICARUS_LIB" -g2012 -s tb -o simulation design.sv testbench.sv
verilator --binary --timing --top-module tb -Wno-fatal --Mdir obj design.sv testbench.sv
yosys -Q -T -s unreachable.ys
yosys -Q -T -s contradiction_any_state.ys
```

`ICARUS_LIB` is required only for a relocated Icarus installation. The 32 actual seeded invocations per simulator use the following argument pattern for each integer seed in `seeds.json`:

```sh
vvp simulation +seed=1 +directed=0
obj/Vtb +verilator+quiet +seed=1 +directed=0
```

Replace 1 with each listed seed 2 through 32; do not substitute a simulator-specific random function. The directed invocations are:

```sh
vvp simulation +seed=1 +directed=1
obj/Vtb +verilator+quiet +seed=1 +directed=1
```

Each seeded run has 16 checked short admissions. All 32 sum to 512 per simulator. The directed run repeats 16 short cases and adds one length-fifteen admission: 17 checked, 16 short, 1 long. `merged-results.json` retains per-seed counts and separate directed counts so repeated stimulus is visible. These are original functional counters, not native covergroup or code-coverage metrics.

The full-and-empty expression is a combinational contradiction for any two-state occupancy, not a reachability-dependent condition. `contradiction_any_state.ys` removes the initialization attribute and proves it in one arbitrary state. The corrected `unreachable.ys` also completes induction, omitting `-seq 1` so its base check includes the initial state. Induction is unnecessary for the combinational contradiction. A preliminary arbitrary-state command using `-set-init-def` alone returned an internal SAT assertion; the record preserves that error and the successful command without that option.

Exclusion rationale: 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. This is a configuration decision, not tested debug behavior.

Earlier `unreachable.ys` remains in `earlier-p8/`; the earlier P8 records remain under `../../measurements/printed-hdl/earlier-p8/`. The binary reports a different revision from the official v0.70 tag; no source-to-binary rebuild is claimed.