Wrong configuration, wrong files, shallow bounds

Configuration

A FIFO proven with DEPTH = 4 says nothing about a product that instantiates DEPTH = 6 — especially if the RTL assumes a power of two (as our FIFO in Chapter 6 does). Check:

• Parameters and defines used in the formal run versus those in the real instantiation.
• Generate branches: a parameter value may select completely different RTL.
• Reduced configurations used for complexity (smaller widths/depths) — each needs a written argument why it represents the real one.

A cheap safeguard is an assertion on the parameters themselves in the RTL:

// Elaboration-time check inside sync_fifo: catch illegal configurations early
if ((DEPTH & (DEPTH - 1)) != 0) begin : g_bad_depth
  $error("sync_fifo: DEPTH (%0d) must be a power of two", DEPTH);
end

Files and versions

Formal regressions sometimes compile an old copy of a file, a stub, or a different branch. Print the file list and revision in every run log, and fail the run if the design hash does not match the one in the release.

Shallow bounded proofs

"Bounded proof to 20 cycles" is a pass only if every relevant state is reachable within 20 cycles. A timeout counter that counts to 1,000 before raising an error makes all error-path assertions trivially "pass" at depth 20. Use covers to measure how deep interesting behaviour lies (and see Chapter 10 for counter abstraction).

Tool settings

Check that no assertions are silently excluded (wrong filters, disabled tasks), that X handling is the intended one, and that warnings about ignored constructs (unsupported SVA, ignored initial blocks) are read and understood.