Your colleague says “make a counter that counts events.” What do you build?
You cannot build from that sentence. It names no widths, no reset, no clock edge and no meaning for the word event. Two engineers who start coding from it build two different counters, and both call theirs correct.
The way out is a specification, which means a written contract that states what the design must do. A testable specification goes one step further: each behaviour in it can be turned into a check that passes or fails. This lesson walks through one for the course running example, mini_controller, a 4-bit event counter.
Register-transfer level (RTL) is hardware described as registers and the logic between them. You write RTL against the spec, and a verification engineer writes a testbench against the same spec. When the two of you read the same words independently, any disagreement exposes a bug or a gap while it is still cheap to fix.
A testable spec has four parts. The interface table names every signal with its direction, width and meaning. The behaviour table states what happens on each clock edge, one row per condition, with the first matching row winning. The acceptance criteria number each checkable claim. The assumptions state the reset type, the clocking, the priority order and the latency, so no reader has to guess them.
The figure below shows the path from a vague request to a buildable plan. Look at the four stages from left to right: each one removes one guess the previous stage left open.
The listing below is the full specification of mini_controller. Read it slowly: every later lesson in this course checks against this document, never against the design code.
# mini_controller specification
Counts accepted events. Written before the RTL; the testbench's reference model and the Python
golden model are both written from this table, not from the RTL.
## Interface
| Name | Direction | Width | Meaning |
|---|---|---|---|
| `clk` | in | 1 | Rising edge clocks everything |
| `rst_n` | in | 1 | Synchronous reset, active low. Takes effect at the next rising edge |
| `event_valid` | in | 1 | One event is offered this cycle |
| `clear_count` | in | 1 | Force the count to zero |
| `count` | out | 4 | Current count. Changes only after a rising edge |
## Behaviour (one row per rising edge, first match wins)
| `rst_n` | `clear_count` | `event_valid` | Next `count` |
|---|---|---|---|
| 0 | x | x | 0 |
| 1 | 1 | x | 0 |
| 1 | 0 | 1 | count + 1, wrapping 15 to 0 |
| 1 | 0 | 0 | count (hold) |
## Acceptance criteria
1. Reset to 0 at the next rising edge, from any count, even when `clear_count` or `event_valid` is high.
2. Exactly one increment per rising edge with `event_valid` high.
3. Wraps from 15 to 0.
4. `clear_count` wins over `event_valid`.
5. Holds its value (including nonzero values) when idle.
6. Does not change between rising edges (reset is not asynchronous).This listing is the contract every later check in this course refers back to.
The interface table fixes five signals. The clock input, clk, times everything on its rising edge. The reset input, rst_n, is synchronous and active low, which means it takes effect at the next rising edge while it sits low, not the moment it changes. The event_valid input offers one event per cycle, clear_count forces the count to zero, and the 4-bit output count reports the current value.
The behaviour table is written so a testbench can follow it row by row. Each rising edge uses the first row that matches: reset wins over everything, then clear, then counting, then holding. The wrap rule sits inside the counting row, where the count moves from 15 to 0, and the hold row keeps the value when the design idles.
The six acceptance criteria turn those rows into numbered checks. Each one names a stimulus and the exact expected result, so a testbench can report a failure against a numbered line. The assumptions are short because the tables already carry them: synchronous reset, one edge per decision, stated priority, and outputs that change only after a rising edge.
Compare that contract with the request you started from:
> Design a counter that counts events. It should reset when needed and be fast.
Hunt the ambiguities before you code. Each item below names one gap, the question you would ask, and the decision the real spec made:
How wide is the count? You would ask what the largest value is. The spec fixes 4 bits, so the count holds 0 to 15.
What happens past the largest value? You would ask whether the counter wraps or stops. The spec wraps from 15 to 0 in the counting row.
What kind of reset? You would ask whether reset is synchronous or asynchronous, and which level is active. The spec states synchronous and active low, taking effect at the next rising edge.
Who wins when inputs collide? You would ask what happens when reset, clear and an event arrive together. The spec orders them: reset first, then clear, then count, with the first matching row winning.
When does the output change? You would ask whether the count moves before or after the clock edge. The spec changes the output only after a rising edge, so nothing moves between edges.
What is an event? You would ask what physical signal counts as one event. The spec defines it: event_valid high during a cycle offers exactly one event, counted once at the next edge.
Notice the pattern. Every ambiguity becomes a question, and every question earns a written answer before anyone codes. That is what testable means: no behaviour left for the reader to invent.
The table below works one short run by hand against the spec. It is illustrative: a small example chosen to touch every row of the behaviour table, not a measurement from any tool. Walk each edge through the table and confirm the count before reading the last column:
Edge | Inputs at the edge | Count after the edge | Which row decided |
|---|---|---|---|
0 |
| 0 | Reset, from any state |
1 |
| 1 | Count |
2 |
| 2 | Count |
3 |
| 3 | Count |
4 |
| 0 | Clear wins over the event |
5 |
| 1 | Count |
6 | idle, all low except | 1 | Hold |
7 | idle again | 1 | Hold |
Edge 4 is the one to study. Two inputs ask for opposite things, and the priority order decides: clear sits above counting, so the count returns to 0 and the event is ignored. Edges 6 and 7 test the hold row, which keeps a nonzero value while idle.
rst_n is low while clear_count and event_valid are both high. What is the count after that edge?0, by the reset row. Reset is checked first and matches regardless of the other inputs, so clear and the event never get consulted. Whenever inputs collide, read the table from the top and stop at the first match.
Writing the spec after the RTL. A document written from finished code describes what you built, including its bugs, instead of what was wanted. Write the spec first, then let the testbench and the design disagree about it.
Acceptance criteria that cannot fail. A line such as “the counter works correctly” passes on any design and catches nothing. Each criterion needs a stimulus and an exact expected value, the way the six numbered lines above do.
Mixing what with how. A spec that names registers, adders or code structure stops describing behaviour and starts dictating implementation. State what each edge must produce; the microarchitecture lesson decides how the logic produces it.
Rule: if you cannot turn a requirement into a failing check, it is not a requirement yet.
Because several rows can match one edge: reset with an event, or clear with an event. Reading from the top and stopping at the first match gives every collision exactly one answer, and the testbench can copy that rule line for line.
The wrap criterion, number 3. Count up to 15 with valid events, then offer one more event: the spec demands 0 and a saturating design still shows 15.
Five gaps to name: (1) what counts as a pulse, a rising edge or a high level, and how long it must last; (2) what programmable means, a limit value, its width, and how software sets it; (3) when the flag rises and what clears it, level or single cycle, held or self-clearing; (4) the counter width and whether it wraps or stops at the limit; (5) the reset type, polarity and priority against counting, plus which clock edge times everything. Each gap needs the same treatment as above: a question, then a written answer with stimulus and expected value.
A testable spec turns each behaviour into a check with a stimulus and an exact expected value.
Interface table, behaviour table with first match winning, numbered criteria and stated assumptions leave no reader guessing.
Every ambiguity becomes a question with a written answer before anyone codes.