Formal pays back fastest on small control logic with a large state space: few signals, many interleavings. Five targets recur across projects, each with a typical bug that random simulation rarely hits.
Target | Why formal wins | Typical bug it finds |
|---|---|---|
FIFO flags and handshake control | Few signals with deep interleavings: safety plus bounded response | A read and a write on the same edge at full: the write is refused but the count still increments |
Arbiters | Fairness and mutual exclusion across every request pattern | Two grants in one cycle when both requests rise on the first edge after reset |
Finite-state controllers | Deadlock and livelock checks that no seed can cover | Abort and done on the same edge send the FSM to a state with no exit |
Reset sequences | Every reset timing across many cycle combinations | An output pulses for one cycle when reset releases on the same edge as a request |
Safety invariants | One missed corner is costly, so exhaustive coverage matters | A locked register accepts a write issued on the same edge the lock is set |
Read it top-down. A cover miss usually means an assumption is too strong, so you go back and weaken it before trusting any pass. A counterexample is either a real bug or an illegal input the assumptions forgot; decide which before you edit anything.
Pair each obligation with exact-trigger and scenario covers. An assert establishes its rule over the checked scope; a cover witness shows that its named sequence is reachable. A bounded cover miss is inconclusive beyond that search depth.
// snippet: runs in a formal tool, not in simulation
// FIFO safety and the blocked-offer response contract used below.
// req = wr && full, gnt = wr && !full (sampled acceptance).
// Source holds wr and wdata through acceptance; no cancellation except reset.
// Consumer supplies rd at every sampled full edge (service gap = 0).
assert property (@(posedge clk) disable iff (!rst_n)
!(fifo_full && fifo_empty));
assert property (@(posedge clk) disable iff (!rst_n)
(wr && fifo_full) |-> ##[1:8] (wr && !fifo_full));
assume property (@(posedge clk) disable iff (!rst_n)
(wr && fifo_full) |=> (wr && $stable(wdata)));
assume property (@(posedge clk) disable iff (!rst_n)
fifo_full |-> rd);
cover property (@(posedge clk) disable iff (!rst_n)
wr && fifo_full); // exact response antecedent
cover property (@(posedge clk) disable iff (!rst_n)
(wr && fifo_full) ##1 (wr && !fifo_full));The problem. The second assert promises that a write blocked by a full FIFO is accepted within eight cycles. FIFO depth does not justify that number; the consumer does. Eventual fairness (the reader reads some day) allows an arbitrarily late read, so it cannot justify any number at all.
The assumption. Define S as the most extra full edges the consumer may let pass before it reads. The second assume above, and the bench below, enforce S = 0: the reader reads at every edge where full is high.
The timing. Read pre-edge values at the edge where the write is blocked (k) and the edge after it:
Edge | Pre-edge full / wr / rd | Acceptance | After NBA |
|---|---|---|---|
k | 1 / 1 / 1 | read only; open blocked-write obligation | count 8 to 7; full=0 |
k+1 | 0 / 1 / any | held write accepted; obligation discharged | count follows accepted operations |
The bound. At edge k the FIFO refuses the write even with rd high, accepts the read and drops the count. At k+1 full is low and the held write goes in. So a blocked write waits at most S + 1 sampled cycles, which is 1 here. The bench measures exactly that: its maximum wait is 1.
Eight is looser. ##[1:8] passes whenever S is 7 or less, so with S = 0 it is correct but weak: a change that added up to seven cycles of latency would still pass. If S really were 7, eight would be the tight bound for this flag policy. Registered flags or a different boundary policy change the timing table, so derive the bound again.
Only blocked offers open this response window; an offer accepted immediately needs no future grant. Reset cancels pending work; withdrawal during a stall is a contract failure. The source must hold both wr and data through the accepting edge, as in the valid/ready contract.
Three writes raise the count to 3, then reads bring it back down to 1. empty is high only in slot 0 and full never rises.
Slot 0: reset, empty 1, full 0.
Slot 1: first write, count 1, empty 0.
Slot 2: second write, count 2.
Slot 3: third write, count 3.
Slot 4: one read, count 2.
Slot 5: write and read together, count stays 2.
Slot 6: read again, count 1.
Depth alone does not decide it. With a held offer and this pre-edge full policy, an accepted read within S extra cycles gives acceptance within S+1 cycles. Eight requires S <= 7; eventual fairness alone is insufficient.
full and empty are both low. Is the FIFO half full?Not necessarily. The pair only forbids the both-high combination. A depth-8 FIFO with count 2 reads the same as count 6 on these two flags.
It establishes exercise in simulation or a reachability witness in formal. The flag invariant can be proven separately even if a bounded cover search misses full.
A depth-8 FIFO with bounded service and a persistent producer: a directed fill/stall/accept prefix, 5000 LFSR cycles and a bounded pending-offer drain.
module fifo_safety #(
parameter int DW = 8,
parameter int DEPTH = 8 // must be a power of two, at least 2
) (
input logic clk, rst_n,
input logic wr, rd,
input logic [DW-1:0] wdata,
output logic [DW-1:0] rdata,
output logic full, empty
);
// Width guard ($clog2(1) is 0, so [$clog2(DEPTH)-1:0] would be [-1:0]).
localparam int AW = (DEPTH > 1) ? $clog2(DEPTH) : 1;
localparam logic [AW:0] FULL_AT = DEPTH;
logic [DW-1:0] mem [DEPTH];
logic [AW-1:0] wptr, rptr;
logic [AW:0] count;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin wptr <= '0; rptr <= '0; count <= '0; rdata <= '0; end
else begin
if (wr && !full) begin mem[wptr] <= wdata; wptr <= wptr + 1'b1; end
if (rd && !empty) begin rdata <= mem[rptr]; rptr <= rptr + 1'b1; end
case ({wr && !full, rd && !empty})
2'b10: count <= count + 1'b1;
2'b01: count <= count - 1'b1;
default: count <= count;
endcase
end
end
assign full = (count == FULL_AT);
assign empty = (count == '0);
endmodule
Testbench run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It uses a depth-8 FIFO with bounded service and a persistent producer: a directed fill, stall and accept prefix, 5000 LFSR cycles and a bounded pending-offer drain. Its checks are not formal or physical signoff results.