EC-21.2 Assertions, Coverage, and Knowing When Verification Is Finished

What this is and why it exists

The hardest question in verification is when to stop, and the honest answer is a number.

Without one, teams stop when the schedule runs out and call that finished. With one, stopping is a decision that can be defended, reviewed and disagreed with. That is the whole purpose of coverage.

Assertions serve the other half. They turn an assumption living in somebody's head into a check that fires wherever it is violated, including in tests written for something else entirely.

The vocabulary

• Assertion — a statement of a rule the design must always obey.
• Immediate assertion — one checked at a single instant.
• Concurrent assertion — one checked continuously across clock cycles.
• Sequence — a pattern of events over time that an assertion can refer to.
• Code coverage — which lines, conditions and states the tests reached.
• Functional coverage — which interesting situations actually occurred.
• Coverpoint — a hand-written record of one situation worth reaching.
• Formal verification — proving a property for every possible input.
• Waiver — a documented decision not to cover something, with a reason.

The mental model

An assertion is an invariant written next to the logic it constrains. The reset must never be asserted for one cycle only. The two request lines must never both be high. Writing these down converts an assumption into a check, and the check runs on every test forever.

Most assertions get written after a bug. The habit worth building is writing them before, as the specification is read, because that is when the assumptions are conscious.

Some rules are about one instant and some are about a relationship across several cycles. Immediate assertions handle the first. Concurrent assertions with sequences handle the second, and they are where assertions start earning their cost. Multi-cycle protocol rules are exactly what a reviewer cannot check by eye.

Coverage comes in two kinds and they answer different questions. Code coverage says which parts of the source the tests reached. It is necessary and not sufficient: full code coverage against a misread specification is a design thoroughly tested against the wrong requirement.

Functional coverage is written by hand from the specification. It records which interesting situations actually occurred: the buffer full at the same moment as a reset, the retry path taken twice in a row. It is the only measure connecting test effort to intent.

Formal verification proves a property for every possible input rather than for the ones you tried. On small control logic this is decisive and fast. On large data paths it does not finish. Knowing which problems fit is most of the skill in using it.

Closure is the argument that assembles all of this. Coverage numbers, a list of waived items with reasons, and a record of what the last failures were. A team that cannot produce those three things has stopped rather than finished.

What you should now be able to explain or do

• Write an assertion for a rule that spans several clock cycles.
• Explain the difference between code coverage and functional coverage.
• Say why full code coverage does not mean a design is correct.
• Decide whether a given property is a good candidate for formal proof.
• Assemble the evidence that justifies calling verification complete.
• Explain why a waiver needs a written reason to be worth anything.

Check yourself