A full physical system cannot be verified directly. It is too large, too analog, too coupled to itself, an object where every wire hears every other wire and no boundary holds still. So we abstract. Reality becomes a board model, the board becomes an SoC model, the SoC becomes a set of IP blocks, the IP becomes RTL. Each step deletes degrees of freedom so a proof can terminate. Then we ask the tractable model to tell us how the intractable thing will behave. We make the chip less like a chip in order to check it, and then we trust the check to predict the chip.
Say the descent out loud, because stated plainly it sounds like what it is. We have a physical thing we cannot hold in one thought, so we replace it with a smaller thing we can. Then we replace that with a still smaller thing. We keep going until we reach a description the tools can close over in an afternoon, and we call the closing a result. The result is true. It is true of the description. The open question, the one the schedule never has a column for, is whether the description was still a description of the chip by the time it became small enough to prove.
This is not a complaint about any one tool. It is the shape of the whole enterprise. Verification is possible only because we agree, at every layer, to stop looking at some of what is there. The agreement is what makes the problem finite. The agreement is also, at every layer, the place where a failure can hide in plain sight, present in the metal and absent from the model, waiting on the far side of a boundary we drew before we knew where the trouble would be.
Abstraction is deletion, not simplification
There is a comfortable word for what we do to the chip on the way down, and the comfortable word is misleading. We say we simplify it, as if we were tidying a diagram so a human could read it, leaving the substance intact and only clearing away clutter. That is not what happens. To make a model checkable, we do not tidy the chip. We remove things from it. We delete degrees of freedom that the physical part will still possess, and we delete them on purpose, because their absence is exactly what lets a proof terminate before the heat death of the schedule.
Watch the deletions accumulate as we descend, each one buying a piece of tractability at the price of a piece of truth.
- Reality to board model. We delete the rest of the world. Temperature settles to a corner. Vibration, aging, the neighbouring board, the connector that oxidises in year three, all gone. The model gains a boundary; the boundary is a fiction we chose.
- Board to SoC model. We delete the supply network's stubbornness. Rails go flat and ideal, decoupling behaves, the ground is one node. The model gains a clean power assumption the copper will not honour.
- SoC to IP. We delete the interfaces' bad days. Links always train, resets arrive together, clocks are present and periodic, neighbours keep their promises. The model gains blocks that can be reasoned about one at a time.
- IP to RTL. We delete time and analog. Signals become logical values that change on edges; a wire is zero or one and never in between, never late, never metastable. The model gains a form a solver can close over.
Each rung down the ladder makes the model more checkable and less true, and the two move together by construction. You cannot buy the tractability without paying the deletion. That is not a defect in how we build models. It is what a model is. And it means that every abstraction boundary is a bet, placed before we know the outcome, about what does not matter. When we flatten the supply to a flat rail, we are betting that the droop we deleted will not decide anything. When we make the reset arrive everywhere at once, we are betting that the raggedness we deleted has no consequence worth checking. We place these bets thousands of times per design, most of them silently, most of them correctly, and we place them all before the silicon exists to tell us which ones were wrong.
The same five layers, read both ways. Everything the left ladder removes to make the proof possible, the right ladder demands the silicon survive. The dashed rungs are the boundaries: each is a bet about what does not matter, placed before the metal can answer.
The reversal: silicon restores everything
Now turn the ladder over, because manufacturing does. When the part comes back, it does not arrive holding our abstractions. It arrives holding everything we deleted to build them. The RTL we proved is now a block sitting on supplies that sag and recover. The block we closed in isolation is now an SoC on a board that rings and reflects. The SoC we signed off is now a board inside a system that heats, ages, and shares its rails with strangers. Every degree of freedom we removed on the way down is restored, all at once, on the way up, and none of it asks permission.
Here is the shape of the paradox, fully formed. The failures we are hunting can sit precisely in the details we deleted to make the hunt tractable. And by construction, our verification cannot see them, because we removed them on purpose before the verification began. The blind spot is not an oversight we could have caught with more diligence at the same layer. It is a structural consequence of how the layer was made checkable. We did not miss the droop; we defined a model in which droop was not a thing that could be represented, and then we proved that model clean. The proof is valid. It is valid over a world we constructed to exclude the failure.
This is the uncomfortable inversion at the centre of the discipline. A clean verdict is evidence that the model was consistent, thorough, and closed. It is not, and cannot be, evidence that the model contained the thing that will end the product. The two claims feel like one claim when the dashboard is green. They are different claims, and the distance between them is exactly the height of the ladder.
The detail you deleted is the bug you ship
This is not a thought experiment. It has a face, and the face is a specific class of check that a specific model never formed.
On cva6, our static timing model represented asynchronous set and clear pins in a way that never created the checks for recovery and removal on those pins. Recovery and removal are the class of timing check that speaks to how a reset releases: how long an asynchronous control must be stable relative to a clock edge as it deasserts, so that the flop it feeds comes out of reset cleanly rather than resolving late. On cva6, that class of check was not weak, and it was not failing. It was absent. The pins were modelled such that the checks simply never formed, and so there were 6,685 checks that did not exist to be run.
$ vsta report cva6 --endpoint-coverage async recovery / removal checks : 0 formed # a class of 6,685 checks that never came into being # the timing run was clean over a class it never represented: # recovery / removal, the checks that speak to how a reset releases.
Read what happened with care, because the ordinary reading gets it wrong. We did not run a check and get a pass we should not have trusted. We did not skip a check that a stricter setup would have run. The model had never formed the check at all. There was nothing to run, and, worse, nothing to report as missing, because a check that never exists leaves no gap where a tool can point and say here is a hole. The absence was total and quiet. The timing report was clean, and it was clean precisely over the behaviour it had no representation for.
This is a modelling choice, the kind every abstraction makes, and it should be read as a defect in that choice rather than as a clever decision to buy tractability. The pins were folded into the build in a form that carried no recovery or removal semantics, and the checks that would speak to reset-release behaviour were therefore never in the model. The count, 6,685, is the size of that absent class once the representation is corrected so the checks can form. It is not a measurement of any board phenomenon, and it is not a prediction that 6,685 things will go wrong. It is the number of checks the abstraction had deleted before verification began.
And the reversal is right there in the silicon. The manufactured die still has asynchronous set and clear pins. Those pins still release on their own schedule, flop by flop, as reset deasserts across a physical net with physical delay. The behaviour is present in the metal. The class of check that would speak to that behaviour was not present in the model. The proof was clean over a region it did not contain, and the region it did not contain is a region the chip inhabits every time it comes out of reset.
Who validates the abstraction itself?
Follow the question one rung deeper, past any single model, and it turns into the one that has no easy floor. Every stage in the flow inherits the deletions of the stage beneath it. RTL verification trusts that the RTL abstraction kept what mattered when it deleted analog and time. Gate-level trusts the library models. Timing trusts the constraints. Signoff trusts them all. Each layer proves something inside the frame the layer below handed up, and each layer takes the fidelity of that frame as a given, because checking it is not the layer's job and, more to the point, not within the layer's reach.
So ask the question the flow never assigns to anyone: who validates the abstraction itself? Not the logic inside it, which the tools check with great care, but the boundary of it, the decision about what the model was allowed to leave out. The RTL simulator cannot tell you whether the RTL abstraction deleted something the silicon will need. It has no representation of the deleted thing; that is what deletion means. The timing tool cannot tell you whether the constraint you wrote deleted a check that should have formed. It works inside the constraints, not above them. The faithfulness of an abstraction is a property that lives one level up from the abstraction, and the proof that runs inside the abstraction cannot reach up to inspect the very frame that bounds it.
This is the load-bearing sentence of the whole essay, so let it stand by itself. A proof is only ever as complete as the layer it stopped at was faithful, and the faithfulness of an abstraction is exactly the thing the proof above it cannot check. The cva6 case is a clean instance. The timing run was internally sound. Every check it formed, it formed correctly. Its incompleteness lived entirely in the frame, in the modelling choice that decided a class of checks would not exist, and no amount of rigor inside the run could have reached the choice that shaped the run. You do not find that kind of gap by verifying harder at the layer that has it. You find it by standing at a different layer and asking what this one was allowed to forget.
What if the chip were treated like a chip?
There is a countermove, and it is worth stating precisely, including where it stops. The countermove is not to abandon abstraction, which is not an option, because there is no verifying the full physical system directly and there never will be. The countermove is to refuse to stop at the most tractable rung merely because it is the most tractable, and to deliberately re-inject some of the conditions the upper abstractions smoothed away, so a proof that would otherwise close over an idealised world has to face a rougher one.
Carry verification across RTL and gate level rather than declaring victory at the layer where the solver runs fastest. Then put back, on purpose, the degrees of freedom the descent removed:
- A clock that vanishes. The RTL assumed a clock always present and periodic. Let it stop for a window and resume, and check what the logic does across the gap the model never had.
- A reset that releases raggedly. The model released reset everywhere at once. Let it deassert flop by flop, across a net with delay, and see whether recovery and removal were the checks that mattered.
- A link that fails to train. The testbench always brought the interface up. Let training fail, and check whether the block downstream has any notion of a neighbour that never arrived.
- A supply that droops. The timing assumed a flat rail. Let it sag mid-transaction and recover, and see which paths the flatness was quietly protecting.
None of these is exotic. Not one requires a phenomenon anyone would call obscure. Each is simply a degree of freedom that an abstraction removed to make a proof close, restored on purpose so the proof has to meet it. A clock stops. A reset is ragged. A link fails to train. A rail droops. These are the ordinary weather of a working board, and the only reason they feel like edge cases is that our models deleted them so early that we stopped counting them as part of the chip.
And here is the limit, stated without softening, because a countermove sold as a cure would be its own kind of deletion. You can never put everything back. The instant you re-inject the droop, you have chosen a droop profile, and the profiles you did not choose are a fresh deletion. Re-injecting the ragged reset means choosing an ordering, and the orderings you did not enumerate are gone again. Every restoration is itself an abstraction, with its own boundary, its own bet about what does not matter. Abstraction is not the enemy that a braver methodology defeats. It is the only way through, at every layer, including the layer where you thought you were putting reality back. The work is not to escape abstraction. The work is to keep asking, at each boundary, what this frame deleted, and to move the boundary toward the failure rather than away from it.
The question the board will not ask
So the question at a tapeout is never only the one the dashboard answers. The dashboard answers did the model pass. The question underneath it, the one that decides whether the pass predicts the part, is different and heavier: what did the model delete to become provable, and does the silicon care about the deleted thing? On cva6, the model passed, and the silicon has asynchronous set and clear pins that release on their own schedule, and the checks that would speak to that release were never in the model. The pass and the pins are both facts. They are facts about two different objects, and the ladder is the distance between them.
This is the one place a WIOWIZ run belongs in the argument, not as a pitch but as a demonstration that the deletion can be made visible instead of silent. A timing tool that reports 0 formed for a class of checks, and names the 6,685 that its input never brought into being, is doing something a clean report does not: it is converting a silent deletion into an explicit one, handing a person a boundary to weigh rather than a green cell to trust. The value is not that the number is alarming. The value is that the absence has a shape, and a shape is something an engineer can decide about.
We remove reality to make verification possible, and then the chip has to survive the reality we removed. A clean result over a deleted detail is not a wrong answer. It is a correct answer to a question the board will never ask. The discipline advances not when a proof gets stronger inside its frame, but when someone stands one layer up and asks what the frame was allowed to forget, and moves the boundary toward the silicon before the silicon moves it for them.