A verification engineer writing checks for a FIFO reaches the sentence "the FIFO asserts full when it cannot accept more data" and stops. Does full assert in the cycle the last slot fills, or the cycle after? Can a push and a pop in the same cycle be accepted when it is full? The designer has already decided, and so, silently, has the engineer writing the scoreboard. If they decided differently, someone will find out later. If they decided the same wrong way, nobody will.
What are specification bugs, and how can they be found when every check is written against the specification?
The obvious view is that the specification is the reference: verification checks the design against it, and the specification is correct by definition. That makes specification bugs invisible to verification by construction. A check written from a wrong sentence enforces the wrong behaviour, and a check written from an ambiguous sentence enforces one reading out of several. The only way to catch them is to treat the specification itself as something to verify.
Kind | Example | What happens |
|---|---|---|
Wrong | A register reset value that contradicts the boot software's assumption | The design matches the document; the system fails |
Ambiguous | "Full when it cannot accept more data": same cycle or next? | Designer and verifier pick different readings, or the same wrong one |
Incomplete | Nothing says what happens to a packet in flight when its port is disabled | Each team invents behaviour; nobody checks it |
Contradictory | One section says errors are counted per input, another per output | Whichever section the designer read wins |
Writing a check forces precision: if a sentence cannot be turned into an assertion or a model, it is not yet precise (Part 2).
Independent readings disagree: when the model and the design differ, ask which one matches the specification, and whether the specification is clear.
Questions are bugs: every question raised while writing checks is filed against the specification and answered in writing.
Corner questions: what happens at reset, at limits, on errors, and when two things happen at once? Specifications are most often silent exactly there.
DCRouter's own specification shows how much precision takes. Compare a vague version of one rule with the one the course uses:
Vague: "The router counts errors in ERR_CNT."
Precise: R9. ERR_CNT[i] counts errors of input i, saturating at 255;
a write clears only that counter.The vague version leaves four questions open: per input or per output, what happens at 255, how it is cleared, and whether clearing one clears others. Three of the Bug Zoo's bugs live in exactly those questions.
Practice | Purpose |
|---|---|
Specification review with verification present | The people who must write checks ask the questions designers skip |
Filing ambiguities as specification bugs | Answers become written, versioned rules instead of hallway decisions |
Executable specifications and reference models | A model forces every rule to be precise enough to run (Part 2) |
Validation against real use | Catches specifications that are precise but wrong (lesson 0.1) |
A DMA specification (illustrative) said a transfer "completes when all data has been written". The designer raised the completion interrupt when the last write left the engine; the verification model raised it when the last write response returned. The scoreboard flagged a mismatch, and the review that followed found the real question: could software read the data as soon as the interrupt arrived? It could not, with the designer's reading. The fix was a specification change and a design change; without the second, independent reading, it would have been a silicon bug.
The specification's: it is ambiguous. File it, get a written answer, then fix whichever of the design or model is wrong.
Every check enforces the specification, so a design that matches a wrong specification passes; only validation against the real need can show it.
Specifications fail by being wrong, ambiguous, incomplete or contradictory.
Verification against the specification cannot see these bugs, so the specification must itself be verified.
Writing checks forces precision: every question raised is a specification bug to file and answer.