Assumptions should model realistic environment contracts. Every strong assumption maps to an interface or protocol guarantee.
Constrain illegal stimulus, but keep legal stress behavior available.
Tag and review assumptions with the same rigor as assertions.
Periodically rerun with reduced assumptions to detect over-constraint.
An implication with a dead antecedent holds for free. If req never fires, req |-> ##[1:8] gnt passes while proving nothing about the grant logic.
Cover the exact antecedent: cover property (@(posedge clk) disable iff (!rst_n) req);. In simulation, zero hits mean non-exercise in that run. In formal, a bounded miss means no witness within that depth; only a complete unreachability result establishes that no legal trace triggers it. A separate property proof still establishes the implication under its assumptions, possibly vacuously if the trigger is unreachable. A stricter req ##1 gnt cover may miss even when req is reachable.
The following table describes finite simulation runs, not formal reachability or proof results.
Run | Requests seen | Property result | Meaning |
|---|---|---|---|
Idle, 200 cycles | 0 | Holds | Vacuous on this run: response unexercised |
Stressed, 2000 cycles | Many | Holds | Exercised: the window is checked |
No request ever fires, so the implication holds without checking anything. The grant in slots 3 and 4 answers nothing.
Slot 1: idle, req 0, gnt 0.
Slot 2: still idle.
Slot 3: stray gnt with no req.
Slot 4: stray gnt continues.
Slot 5: quiet again.
Slot 6: quiet. The implication never fires, so it never fails.
The proof covers a smaller world than the chip lives in. Real back-to-back traffic is never checked, so its bugs survive sign-off.
req misses. What was established?Identify the method: simulation has not exercised the response; bounded formal cover has found no witness within its depth. A separate unbounded property proof still proves the implication under its assumptions. Proven trigger unreachability explains vacuity and warrants assumption review.
Whenever a proof passes too easily or the environment contract changes. Weaker assumptions that still pass raise confidence. New failures point at over-constraint.
The same grant pipeline under two environments: 200 idle cycles, then 2000 LFSR cycles, each with cover counts.
module grant_delay (
input logic clk, rst_n, req,
output logic gnt
);
logic r1, r2;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin r1 <= 1'b0; r2 <= 1'b0; gnt <= 1'b0; end
else begin r1 <= req; r2 <= r1; gnt <= r2; end
end
endmodule
// For known inputs stable across the edge and reset released on a falling edge:
// pre-NBA samples model req |-> ##[1:8] gnt; observe violation after NBA.
// Each bit records an outstanding request's age, including overlapping windows.
module response_window8 (
input logic clk, rst_n, req, gnt,
output logic violation
);
logic [7:0] pending;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin pending <= '0; violation <= 0; end
else begin
violation <= pending[7] && (gnt !== 1'b1);
if (gnt === 1'b1) pending <= {7'b0, req};
else pending <= {pending[6:0], req};
end
end
endmodule
The idle phase deliberately injects unsolicited grants. The response implication still passes because no request opens a window. A separate no-unsolicited-grant property would fail; do not replace the implication with gnt == 0 during idle. The stressed phase exercises the same eight-cycle obligation and drains outstanding windows before reporting.
Testbench run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It runs the grant pipeline for 200 idle cycles, then 2000 LFSR cycles, with cover counts. The table describes finite simulation runs, not formal reachability or proof results.