The evaluator's checklist, explained

The problem

You are evaluating an IP vendor, and the datasheet says “formally verified.” You ask the obvious question - “do you run formal verification?” - and the answer is yes. You ask “is it covered?” and the answer is yes. Every vendor in the room answers yes to both, including the ones shipping a proof that never explored a single interesting state. The checklist failed before the meeting started, because it asked questions a vacuous proof can honestly pass.

This post is the checklist we would want asked of us. Five concrete items, each one backed by a real artifact from our own Regex Accelerator proof bundle, and the exact follow-up question that turns a vendor’s “yes” into something you can check yourself.

Show the failure

Here is the checklist most evaluations actually run, and why a vendor can pass every line of it honestly while shipping something worthless:

Fluffy question	How a vendor says “yes” and it means nothing	The real ask
”Do you use formal verification?”	One property, over-constrained by an assumption, proves trivially	”Show me the assumption file, and prove the property fails without it."
"Is it covered?”	Coverage counts lines touched, not states reached	”Show me a cover property that witnesses the state your assertion depends on."
"Do you document assumptions?”	Assumptions live inline, mixed into the assertions, never audited	”Show me the assumption file as its own artifact, reviewed on its own."
"Can I trust this artifact?”	The RTL you get is not the RTL that was proven	”Show me the hash. Does the bundle’s manifest match the file in my hands?"
"Can I reproduce your result?”	The proof ran once, on someone’s laptop, with unpinned tool versions	”Give me the seed and the pinned toolchain. I will run it myself.”

It passes every fluffy question, and that is exactly when it is dangerous: a rubber-stamp checklist rewards the vendor who prepared answers, not the vendor who did the work.

Key Lesson: A checklist question that can be answered “yes” without producing an artifact is not a checklist question. It is a formality.

Why it fails

The mechanism is the same in all five rows: the fluffy question asks about the existence of a practice, and the real ask ties it to a specific file in the bundle. If the vendor cannot point at the file, the practice does not exist, no matter what the datasheet says.

We wrote about this failure mode from the inside in what a formal “PASS” has to earn: an over-eager assumption can make a proof vacuously true, because the solver never explores the states where the bug lives, and it still reports PASS. The fix there was structural - assumptions live in their own bound file, separate from the assertions they constrain, so the constraint on a proof can be read in one place instead of hiding inside it. That structural fix is also what makes the assumption row of this checklist checkable at all: if assumptions are not a separate artifact, there is nothing to hand the evaluator.

The fix, five items with a file behind each one

1. Non-vacuity

A property that can never fail is not a proof, it is a tautology. The check: does the antecedent of every assertion actually get exercised, or does an over-broad disable iff or assumption gate it shut? Our shipped SVA for the Regex Accelerator’s NFA lane states the obligation directly rather than assuming it away:

// no match asserted without a started scan
property p_match_requires_scan;
  @(posedge clk) disable iff (!rst_n)
    match_valid |-> scan_active;
endproperty
a_match_scan: assert property(p_match_requires_scan);

Ask your vendor: “Run this property with the antecedent forced false. Does the proof still pass?” If it does, the property was never live in the first place.

2. Cover reachability

An assertion proves a property holds whenever its trigger fires. It says nothing if the trigger never fires. A cover property is the witness that it does - illustrative shape, bound the same way as the assertion it backs:

// illustrative: witness that a deep-rule match is actually reachable
c_deep_match: cover property (
  @(posedge clk) disable iff (!rst_n) match_valid && match_rule_id == DEEP_RULE_ID
);

Ask your vendor: “For the property you just showed me, show me the cover that proves its own trigger is reachable.” No cover, no reachability - just an assertion that may be describing an empty set of states.

3. Assumption discharge

Every assume is a constraint on the solver, and constraints compound. The dual-use macro we ship keeps one contract file honest under both engines - the same text is a solver constraint under formal and a live monitor under simulation:

`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

Because the identical contract runs as a simulation monitor, an assumption that were too strong to be true would fire as an assertion failure the first time real stimulus violated it - the discharge is not a one-time review, it is continuously checked. This is real, shipped machinery, not a description of a hypothetical - see what a formal “PASS” has to earn for the full context.

Ask your vendor: “Point me at the assumption file, separate from the assertion file. Does the same contract run as a checker in simulation?“

4. Hash binding

The RTL you review in a design partner meeting and the RTL that shipped are only the same file if you can prove it. Our provenance chain runs requirement to architecture to RTL to testbench to release, each link a short hash (full SHA-256 manifests ship in the bundle; short hashes here are illustrative):

link	example	hash (illustrative)
requirement	REQ-FUNC-001	a3f1
architecture	arch/nfa_subsys.md	9b22
rtl	nfa_byte_lane.sv	7f3a
testbench	tb_coco/	c41e
release	regex-v1.0.tgz	d0e8

Ask your vendor: “Give me MANIFEST.sha256 from the release, and let me hash the RTL file myself.” If the hash you compute does not match the manifest, you are not evaluating the artifact you think you are.

5. Pinned reproduction

A proof that ran once, on someone’s machine, with whatever tool version happened to be installed, is a claim you cannot check. Ours closes with a fixed regression layer: reproducible seeds, and a full-suite re-run gated on every change before release - the same discipline that let the Regex Accelerator’s cocotb bring-up regression close clean under UVM 1800.2 with a pinned Verilator model.

Ask your vendor: “Give me the seed and the pinned tool versions. I will re-run the regression in my own CI, not yours.”

Key Lesson: Every real checklist item resolves to a file you can open - a property, a cover, an assumption module, a manifest, a seed. If the vendor’s answer is a sentence instead of a file, you have not evaluated anything yet.

Two ways to run the evaluation

A. Trust the summary. Read the datasheet, ask the fluffy questions, accept “PASS” as the whole story. Fast - a design partner call, no bundle to walk. The cost is deferred: you find out what the proof actually covered when the block misbehaves in your integration, and by then the fix is expensive.

B. Open the bundle yourself. Pull the manifest, hash a file, force an antecedent false, re-run the regression on your own machine with the pinned toolchain. Slower up front - it takes an afternoon, not a phone call - but every claim you accept, you have personally checked instead of taken on faith.

We build for evaluators who choose B, because a vendor who cannot survive B was never going to survive your integration either.

Key Lesson: The fast evaluation and the honest evaluation are not the same activity. Budget the afternoon before you budget the integration.

Proving it: grading the checklist against itself

A checklist is only as good as its ability to catch a real gap, so we ran ours against our own bundle the way we’d want an evaluator to. The mutation-testing discipline described in what a formal “PASS” has to earn exists for exactly this purpose: inject a fault, re-run the proof, see whether any assertion fails. A killed mutant means the property set caught the injected bug; a surviving mutant is a named gap. In that campaign, a register slice with an airtight handshake and reset proof still only killed half its injected mutants - every survivor traced to the buffer primitive it instantiated, not the wrapper logic the bench was aimed at. That is the checklist’s item 1 and item 2 working as evidence, not assertion: the gap was found, written down, and is not the sentence you get from a vendor who only ran the fluffy checklist.

From “it works” to “it ships”

The checklist is not a one-time gate, it is a release contract:

• Manifest regenerated per release. MANIFEST.sha256 is rebuilt and re-signed on every RELEASE.sig, not carried forward from an earlier tag.
• Assumption file reviewed on its own, every change. Not bundled into an assertion diff where a widened constraint can hide.
• Cover set grows with the assertion set. A new property ships with a cover proving it is not vacuous, in the same commit.
• Regression seed and tool versions pinned in the same manifest as the RTL. So “reproduce this” means one command, not an email asking which Verilator version was used.
• Mutation score reported per block, not averaged across the design. A single well-tested cell hiding a weak one is the failure mode the checklist exists to catch.

Lessons

A verification claim you cannot check is marketing. A verification claim mapped to a specific file - a property, a cover, an assumption module, a manifest hash, a pinned seed - is engineering, and the difference is entirely in whether you asked for the file.

The bundle, and where to go next

Every item on this checklist maps to something you can open on the evidence page: the properties in section 2, the traceability chain in section 3, the provenance hashes in section 5, and the full bundle layout in section 6. We would rather hand you the manifest than the summary.

The two posts this checklist draws from, if you want the engineering underneath each item:

• A passing testbench proves nothing - until it can fail - the hard-gate discipline that makes a 66-of-66 UVM result believable.
• What a formal “PASS” has to earn - the vacuity trap, the assumption-discharge macro, and the mutation-testing numbers referenced above.

Can I re-run your proofs in my CI?