Quality checks: is the proof worth anything?
A wall of green "proven" results feels great — and proves nothing until it survives these checks:
| Check | Question it answers | How |
|---|---|---|
| Cover review | Is the interesting behaviour reachable? | All covers hit; traces inspected |
| Vacuity | Does every implication have a reachable antecedent? | Tool vacuity report, or explicit covers of antecedents |
| Over-constraint | Do assumptions forbid legal behaviour? | Covers of legal scenarios; review assumptions; check assumptions against the neighbour's RTL |
| Mutation | Would a real bug be caught? | Inject small RTL changes; at least one assertion must fail for each |
| COI coverage | Is every piece of logic checked by some assertion? | Tool report of flops/lines in the cone of proven assertions |
| Proof-core coverage | Which logic was actually needed for the proofs? | Stronger than COI; reported by most commercial tools |
Mutation by hand
Even without tool support you can run a manual mutation campaign. For the FIFO, try each of these and confirm that some assertion fails:
| Mutation | Expected to be caught by |
|---|---|
assign do_push = push; (no full check) | a_full_drop, a_data_order, a_count_range |
rptr <= rptr + 2'd2 (with DEPTH=4) | a_data_order |
assign full = (count == CW'(DEPTH-1)); | a_flags only — remove a_flags and this mutant survives, because every other check uses the DUT's own full. Try it! |
Swap the order of + do_push - do_pop into - do_push + do_pop | a_count_inc, a_count_dec |
assign rdata = mem[wptr]; | a_data_order |