What a formal "PASS" has to earn

A formal tool printing PASS is one of the most over-trusted signals in hardware design. A proof is only ever as strong as the property it proved, and most green proofs are weaker than they look: they assume too much, check the wrong thing, or assert something that could never have failed in the first place. This post is about the discipline that makes a formal pass worth the word - and the test we run to catch ourselves when it isn’t.

Structure the bench so the assumptions stay honest

Every property module we bind onto a design is split into three files: the assertions (what must hold), the environment assumptions (what the surrounding system guarantees), and the covers (witnesses that the interesting states are reachable). Each is bound onto the DUT separately, and the original RTL is never modified to make it provable.

The split is not bureaucracy. An assumption is a constraint on the solver, and an over-eager assumption can quietly make a proof vacuously true - the prover never explores the states where the bug lives, and reports success. Keeping every assumption in one dedicated, bound file means the constraints on a proof can be read and audited in one place, instead of being scattered through the assertions they secretly weaken.

One contract, two engines

The upstream protocol contract a prover treats as an assumption is the same contract a simulator should treat as a runtime monitor. So we write it once, behind a dual-use macro:

`ifdef FORMAL
  `define CONTRACT(name, expr) name: assume property (expr)   // constrain the solver
`else
  `define CONTRACT(name, expr) name: assert property (expr)   // watch the live stimulus
`endif

Under formal, a valid-held-until-ready contract bounds the solver to legal traffic. The instant the same files run in a UVM simulation, that line becomes an input-protocol checker that fires if the testbench ever drives an illegal sequence. The formal environment and the simulation environment enforce the same contract instead of drifting apart.

Counting beats is not proving data

Here is the trap that catches most “verified” data movers. A FIFO or a register slice gets a proof that counts accepted versus delivered beats, checks that valid is held stable until ready, and confirms the buffer never overflows. It looks complete. It proves nothing about the data.

A design that quietly swapped two payloads, or inverted a byte lane, passes every one of those checks - the counts still match, the handshake is still well-behaved. What’s missing is a property that follows a value. So we track a symbolic beat: pick an arbitrary beat ordinal as a free constant, capture its payload on the way in, and assert the same-ordinal beat carries that exact payload on the way out. Because the ordinal is free, proving it for “some” beat proves it for every beat - data integrity and FIFO ordering in a single property.

That tracked value has to be arbitrary but constant: arbitrary, so the proof covers every possible payload rather than one lucky value; constant, so it cannot change while the beat is in flight. The usual way to declare such a value is an anyconst signal. The sharp edge worth sharing is that some open-source elaboration frontends silently ignore the anyconst attribute - the signal collapses to a single fixed value, and the scoreboard quietly proves almost nothing.

The sound substitute is a plain register with no reset and no initializer, whose only driver is itself:

logic [W-1:0] tracked;                         // no reset, no initializer
always_ff @(posedge clk) tracked <= tracked;   // only ever assigned its own value

A register the solver never initializes starts at an unconstrained value, so the solver is free to pick any payload. And because the only thing it is ever assigned is its own current value, it keeps that pick for the entire trace. Arbitrary, then frozen - exactly the semantics of anyconst, with no dependence on the attribute being honored.

Put together, the whole scoreboard is about a dozen lines bound onto the design under test. Watch one beat, chosen by its position in the stream, and require it to leave exactly as it arrived:

logic [3:0]   tag;                       // which beat to watch - free constant
always_ff @(posedge clk) tag <= tag;

logic [3:0]   in_idx, out_idx;           // beats accepted / delivered so far
logic [W-1:0] tracked;                   // payload captured at the watched beat
logic         armed, done;

always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin in_idx<=0; out_idx<=0; armed<=0; done<=0; end
  else begin
    if (s_valid && s_ready) begin                       // an input beat is accepted
      if (!armed && in_idx == tag) begin tracked <= s_data; armed <= 1; end
      in_idx <= in_idx + 1;
    end
    if (m_valid && m_ready) begin                       // an output beat is delivered
      if (armed && !done && out_idx == tag) done <= 1;
      out_idx <= out_idx + 1;
    end
  end

// The watched beat must leave carrying exactly what it arrived with.
always_ff @(posedge clk)
  if (rst_n && armed && !done && m_valid && m_ready && out_idx == tag)
    data_integrity: assert (m_data == tracked);

armed and done make the capture and the check fire exactly once, so a counter wrap cannot re-arm the watcher on a stale ordinal. That single assert, proved for an arbitrary tag, is what turns “the counts line up” into “every byte that went in came out, unaltered and in the order it arrived.” The same shape catches a reorder: if beat 5 overtakes beat 4, the ordinal that captured beat 4’s payload sees beat 5’s payload at the output, and the assertion fails.

Grade the grader: mutation testing

Covers prove a property can trigger. They do not prove the property would catch a bug. An assertion can be reachable, non-vacuous, and still too weak to fail on a real defect. The only way to find out is to break the design on purpose.

So we mutate it. Inject a single fault - invert a bit, tie a wire to a constant - re-run the proof, and see whether any assertion fails. A killed mutant means the bench caught the injected bug; a surviving mutant is an assertion gap, written down in black and white. The kill rate is the honest measure of how strong a property set actually is.

We are not flattered by our own first numbers, and that is the point. A register slice whose handshake and reset proofs were airtight killed only half of its injected mutants - and every survivor lived inside the buffer primitive it instantiated, not in the wrapper logic the bench was aimed at. The proof wasn’t wrong. It was aimed at the wrong altitude.

Prove the leaf, inherit at the parent

That mutation result is an argument for hierarchy, made by evidence rather than taste. Verifying a block only through its wrapper leaves the wrapper’s internal primitives under-tested, because the wrapper’s assertions sit too far from the logic doing the work. So the strong, value-level proofs go on the leaf cells; parents that instantiate them inherit that evidence and only need to prove their own composition. Fewer total proofs, and each one aimed where mutations can actually reach.

A PASS with a definition behind it

All of this rolls up into a sign-off tier, and the tier rules are deliberately unkind:

• Vacuity or over-constraint forces a fail outright - it does not matter how many properties “passed.”
• A data mover with no value-level data-integrity proof cannot reach the adequate tier on handshake and occupancy checks alone.
• The top tier requires mutation evidence, not just a clean proof run.
• And the verdict names its engines. If k-induction never closed and only a reachability engine carried the proof, the record says exactly that, rather than laundering it into an unqualified “PASS.”

“Formally verified” is a claim with a definition behind it, and the definition is the product. As with everything we ship: don’t trust the summary. Open the package and check the properties, the covers, and the kill rate.