A chip is not verified because the tests pass — it is verified when you can show what has not been tested is not there. Coverage closure is the discipline of measuring what has actually been exercised, generating stimulus to reach the rest, and using formal methods where simulation cannot go.
DomainSilicon, functional verification
PlatformsFaststream Silicon
ScopeVerification plan to coverage closure
Binding constraintProve the untested space is empty, not ignored
DisclosureRepresentative programme; customer not named
CONTEXT
Where this started.
A complex SoC has a state space no directed test suite can enumerate. Passing tests prove the cases you thought of work; they say nothing about the cases you did not. The bug that escapes to silicon is almost always in the space no test looked at, which is why verification is measured by coverage, not by a passing run.
Closure means building a verification plan that defines what must be exercised, driving it with constrained-random stimulus and checkers, measuring functional and code coverage against the plan, and then hunting the stubborn holes — the corners the random generator rarely hits and the properties only formal methods can prove.
So the work is coverage-driven: a plan that says what 'done' means, an environment that reaches for it, and an honest account of the space that remains, closed by targeted stimulus or formal proof rather than declared closed.
CHALLENGES
4 problems, named.
Stated before any of them had an answer.
01
Passing tests prove little
A green regression proves the imagined cases work; it says nothing about the unimagined ones, which is where escapes hide.
02
Coverage has to be defined
Without a plan that states what must be exercised, coverage is a number without meaning; closure needs a target, not just a metric.
03
Random misses the corners
Constrained-random stimulus covers the bulk quickly and then stalls; the last holes are corners it rarely reaches and needs directing to.
04
Some properties need formal
Certain behaviours — arbitration fairness, deadlock freedom — cannot be closed by simulation and require formal proof.
ARCHITECTURE
How it was built.
Green tests are the start. Coverage closure is showing the untested space has been reached — by stimulus or by proof — rather than left as an unknown.
CONTRIBUTION
What Faststream did.
The scope of the work, rather than a capability list.
Verification plan — defining what must be exercised so coverage has a target and 'done' has a meaning.
Coverage model — functional and code coverage tied to the plan, not a metric collected in the abstract.
Constrained-random environment — stimulus and self-checking that cover the bulk of the space quickly.
Directed corner cases — targeted stimulus for the holes the random generator rarely reaches.
Formal verification — proving the properties simulation cannot close, such as fairness and deadlock freedom.
Coverage closure — an honest account of the remaining space, closed by stimulus or proof rather than waived.
WHAT WAS HARD
The parts that consumed the schedule.
Rarely the subsystem that sounds difficult.
01
Defining 'done' honestly
The plan is the hard intellectual work; a coverage number without a rigorous plan behind it is a false comfort.
02
Chasing the last holes
The final coverage points are where the time goes — corners the random generator almost never hits and that need directed effort to reach.
03
Knowing when formal is the tool
Recognising the properties that simulation cannot close and switching to formal proof is a judgement that separates real closure from a stalled regression.
04
Resisting the waiver
The temptation at the end is to waive the awkward holes; genuine closure means reaching them, because the waived corner is where the escape hides.
OUTCOME
What resulted.
Coverage closed to plan
Functional and code coverage met against a rigorous plan, not a number in isolation.
Corners reached
The stubborn holes closed by directed stimulus rather than left uncovered.
Properties proven
Fairness, deadlock freedom and similar closed by formal methods.
An accounted space
An honest record of what was exercised and how, rather than a green run that hides gaps.
Confidentiality
Customer projects are presented at property, capability, outcome and integration level. Customer names, internal architecture, confidential deliverables and commercial terms are not disclosed. Where a detail would identify a customer it is omitted rather than approximated. More is available under a non-disclosure agreement, within the limits the customer has agreed.
If all the tests pass, why isn't the chip verified?
Because passing tests only prove that the cases someone thought to write work. A complex SoC has a state space far larger than any directed suite can enumerate, and the bug that escapes to silicon is almost always in the region no test examined. Verification is therefore measured by coverage — how much of the intended behaviour has actually been exercised — rather than by a green regression, which proves the imagined cases and nothing about the unimagined ones.
02
What is coverage closure?
It is the discipline of driving measured coverage up to a defined target and accounting for everything that remains. It starts from a verification plan that states what must be exercised, uses constrained-random stimulus with checkers to cover the bulk, measures functional and code coverage against the plan, and then hunts the stubborn holes with directed tests or formal proof. Closure means the untested space has been reached and shown empty, not declared closed or waived.
03
When do you use formal instead of simulation?
When a property cannot be practically closed by simulation. Some behaviours — arbitration fairness, absence of deadlock, certain safety properties — hold over such a large or subtle state space that no reasonable amount of random or directed stimulus proves them. Formal verification proves them mathematically instead. Recognising which properties need formal, rather than grinding simulation against them, is part of reaching genuine closure.