The bug formal verification never saw: anatomy of a composition escape

The problem

Here is a sentence that sounds like the end of the story: “the arbiter primitive is formally verified, so the crossbar built from it is safe.” It is not the end of the story. A leaf-level proof only covers the leaf. The moment a parent module wires that leaf into a bigger design, the parent’s own glue logic can quietly break a contract the leaf’s proof was relying on - and no amount of re-reading the leaf’s report will catch it, because the leaf was never wrong.

This is exactly what happened on a 4-input, 5-output AXI crossbar (vcx_crossbar_core, built around a stream_xbar_arb primitive). The arbiter’s own proof was clean. The crossbar shipped into simulation anyway, and a UVM test caught a protocol violation on the very first live run against a single, fully legal write. Here is how that happens, and what it costs to close it honestly.

Show the failure

The bug lived in vcx_crossbar_core.sv’s accept-gate, the logic that decides whether the core presents a request to the arbiter primitive it instantiates as u_aw_xbar / u_ar_xbar. Curated excerpt, pre-fix, from the escape-closure record (not the full IP source):

// CURATED EXCERPT from vcx_crossbar_core.sv lines 686-698 (pre-fix, RTL-BUG-001).
// This is the accept-gate that withdraws a presented request mid-stall.
// Public-safe excerpt for the composition-escape post - NOT the full IP source.

                .req_target(ar_tgt_idx[i]),
                .req_allow (ar_id_lock_allow[i]),
                .req_fire  (ar_accept[i]),
                .resp_fire (ar_resp_fire[i]),
                .resp_id   (s_axi_init_RID[i]),
                .busy      (ar_id_lock_busy[i]),
                .id_active (ar_id_lock_active[i])
            );

            // ---- Per-port write-outstanding structural credit cap (REQ-ERR-192) ----
            credit_counter #(
                .NUM_CREDITS(OUTSTANDING_DEPTH),
                .INIT_EMPTY (1'b0)

The line that actually broke the contract is not in this excerpt (it sits just above it), but the escape-closure analysis quotes it precisely: the core computes aw_req_valid[i] as a pure combinational AND of live state - s_axi_init_AWVALID[i] && aw_dec_valid[i] && aw_id_lock_allow[i] && aw_credit_avail[i]. It passed every UVM regression the arbiter primitive shipped with, and that is exactly when it is dangerous: a passing regression tells you the cases it covered were fine, not that no case exists.

Key Lesson: A primitive’s own proof only says the primitive is correct. It says nothing about the module that instantiates it, because that module can drive the primitive’s inputs in ways the primitive’s proof never had to consider.

Why it fails

aw_req_valid[i] being a live combinational function means it can flip on any cycle where aw_id_lock_allow[i] or aw_credit_avail[i] changes - including a cycle where the arbiter has already latched that request as pending and is simply waiting its turn to grant it. The arbiter’s own input contract assumes the opposite: once a request is presented, it holds VALID until the arbiter’s s_ready signals grant. The core violates that assumption from underneath:

Cycle	Core presents aw_req_valid[i]	Arbiter’s aw_xbar_s_ready[i] (granted?)	What changes	Result
N	1	0	id_lock_allow and credit_avail both still 1	Request presented; arbiter is still arbitrating, not ready yet
N+1	0	0	id_lock_allow flips to 0	Core withdraws the request the arbiter still considers pending

That table is the whole bug: a request the arbiter is holding as “still there” simply disappears one cycle later, because the accept-gate never latched its decision once presented.

Where the arbiter’s own proof stopped short. stream_xbar_arb ships with a registered formal sweep across several instantiated shapes - but not this one:

NUM_IN x NUM_OUT shape	In the primitive’s registered sweep?	Instantiated by vcx_crossbar_core?
2x2	Yes	No
3x2	Yes	No
3x3	Yes	No
4x4	Yes	No
4x5 (4 targets + DECERR sink)	No, until this escape	Yes

And the core-level bundle only asserted stability on the upstream side of the arbiter (its own request into the arbiter), while reusing the arbiter’s own clean proof for the output side, on the assumption that the arbiter’s input contract was separately guaranteed. It never was, at this shape.

Key Lesson: “The primitive is proven” and “the primitive is proven at the shape you actually instantiate” are two different claims. A sweep over four configurations does not cover a fifth.

The fix, and why “fix in review” is the honest way to say it

The team’s first move was to suspect the primitive itself - the obvious suspect, since the failing signals cross its boundary. They extended stream_xbar_arb’s own formal sweep to 4x5 and 4x6. Both legs passed, unbounded induction, non-vacuous covers. The primitive was exonerated. That negative result mattered as much as the eventual positive one: it told the team where not to spend the next hour.

The real fix belongs to vcx_crossbar_core’s accept-gate: a presented request has to be qualified once, at presentation, and then held stable until the arbiter accepts it - not re-evaluated combinationally every cycle it sits in the arbiter’s queue. That means latching the gate condition rather than continuously deriving it from id_lock_allow and credit_avail, while still preserving the no-grant-without-credit invariant the accept-gate exists to enforce.

As of this writing, that RTL change is in progress and not yet merged. The escape-closure record is explicit about what is done and what is not:

• Formal repro: pre-fix CEX at BMC depth 4, two independent property families
• Primitive-side hardening landed regardless (4x5/4x6 sweep legs now registered, both pass)
• Fix vcx_crossbar_core’s accept-gate (in progress)
• Post-fix PASS on the same properties, re-stamped provenance
• Rebuild the environment simulation to a passing base test

We are not calling this fixed until the last three boxes close. A bug ledger that says “fixed” before the post-fix proof exists is exactly the kind of claim this post is arguing against.

Two ways to draw the composition boundary

A. Assume-guarantee reuse (what shipped here). The core-level proof assumes the arbiter’s own proof covers the arbiter’s output behavior, and only re-proves the boundary the core controls directly. Cheap: the core-level proof stays small, because it is not re-deriving what the leaf already proved. The cost is exactly the failure mode above - the reuse is only sound if the parent never violates the assumption the leaf’s proof depended on, and nothing was checking that on the parent side.

B. Flatten and re-prove monolithically. Verify the whole core, arbiter included, as one flat proof with no trust boundary. This structurally cannot miss a composition-glue bug, because there is no boundary left to violate. The cost is state-space size: a flat proof over the full core has to re-derive everything the leaf already established, and does not scale as more leaves are added.

The fix actually adopted here is a third option in between: keep the composition boundary, but add a confirmatory property that re-tests the specific obligation the reuse was leaning on - the arbiter’s own s-side input, not just the wire to the outside world. That is cheaper than flattening and would have caught this before it shipped.

Proving it

Two new property families went in at the core level. The first re-checks the boundary to the outside world; the second - added after the first counterexample - re-tests the arbiter’s own s-side input, which is exactly the obligation the assume-guarantee reuse was quietly skipping:

// illustrative - reconstructed from the escape-closure record; the shipped SVA file
// (fv_vcx_crossbar_core_awstab.sv) is not part of this curated excerpt.
// Re-tests the arbiter's OWN s-side input, not merely the m_axi_targ boundary.
property p_awxbar_reqvalid_confirm(i);
  @(posedge clk) disable iff (!rst_n)
    (aw_req_valid[i] && !aw_xbar_s_ready[i]) |=> aw_req_valid[i];
endproperty
P_AWXBAR_REQVALID_STABLE_CONFIRM_A: assert property (p_awxbar_reqvalid_confirm(i));

The confirmatory property (P_AWXBAR_REQVALID_STABLE_CONFIRM_A) is the one that actually failed first, at BMC depth 4, on an initiator lane’s own request line into the arbiter - not on the output boundary. Depth 4 is a handful of seconds of solver time; this was a cheap property to write and cheap to run, at exactly the seam where compositional trust was being assumed rather than checked.

Before trusting that counterexample, the team ruled out the obvious false-positive source: a mid-trace reset re-assertion masquerading as a live bug. They added a scratch-only diagnostic constraint forcing reset monotonic (once high, never falls again) and re-ran the same bounded model check at depth 20. The counterexample still appeared, on a different lane index but the same property classes and the same step - reset-independent, and not an artifact of the check itself.

One honest gap remains open: the properties’ cover set was written in the same pass, but this run only exercised assertion falsification (mode=bmc); a separate mode=cover run to prove those covers are actually reachable, rather than just syntactically clean, has not happened yet. That is flagged as a follow-up, not swept under the closure.

Key Lesson: The cheapest property to add is often at the seam between two things everyone already trusts separately. That is precisely where nobody is checking the join.

From “it works” to “it ships”

• Reset independence checked, not assumed. The team re-ran the failing check under a forced-monotonic-reset constraint before accepting the counterexample as real - a five-minute check that rules out an entire class of spurious traces.
• Verify the shape you ship, not a representative one. The primitive’s registered sweep covered four configurations and missed the fifth one actually instantiated. The fix is not “add one more shape” - it is to always include the exact instantiated parameterization in the leaf’s own sweep.
• Exclusion lists are debt with a name on it. The 16-property exclusion list that let this obligation through was a documented, deliberate call (Tier-C debt), not a silent gap - but it should never have contained a composition-discharge obligation, precisely the class of property that stands between “the leaf is proven” and “the parent is safe.”
• The evidence pair is the actual sign-off, not the CEX alone. A pre-fix failure proves the bug is real. It does not prove the fix works. Sign-off needs both halves: fail before, pass after, same property.

Lessons

Suspect the primitive first, and believe a clean re-sweep when you get one - an honest negative result saves you from debugging code that was never the problem. A child module’s assume is a promise; if nothing forces the parent to keep that promise, the promise is not enforced, it is hoped for. The fix for that is always the same shape: turn the child’s assumption into a property the parent is machine-checked against, at the exact seam where the two proofs meet. And the standard this post is trying to hold itself to: every bug that escapes formal should leave formal stronger than it found it - a new property that fails on the pre-fix design and passes on the post-fix one. Here, that pair is still half-built. We would rather say that plainly than round it up.

The bundle, and where to go next

The escape-closure record this post draws from - the bug ledger, the counterexample data, and the pre-fix accept-gate excerpt - is the same kind of artifact the evidence page describes: a proof result is only worth trusting if you can open the file behind it, not just the summary.

Related reads, if you want the machinery underneath this post:

• What a formal “PASS” has to earn - the assume/assert split and the dual-use macro that keeps an assumption honest under both formal and simulation, which is the exact discipline this crossbar’s core-level proof was missing.
• A passing testbench proves nothing - until it can fail - why a green regression is not evidence on its own, the same lesson this bug’s escape into a UVM pass would have taught the hard way.
• The evaluator’s checklist, explained - the assumption-discharge question this whole post is one worked example of.

Can I re-run your proofs in my CI?