Can you take a short specification all the way to a green build on your own?
A new specification sits in front of you: a short interface table, four rows of behavior, seven numbered criteria. There is no RTL yet, no testbench, no Makefile. The starter folder, pulse-counter-starter/ in start-here-examples.zip, holds that spec, a module header full of TODO comments, and the rubric that says exactly what good looks like. Your job is everything between that starting point and a build that passes on a machine you have never touched.
Every file you write answers to the specification, and to nothing else. The golden model translates the behavior table into Python, so a reader can check the rules without reading hardware code. The testbench translates the same table into checks, so the simulation tests the intent instead of repeating your RTL back to you. When the model and the testbench disagree, the spec settles the argument, because both were written from it.
That order matters. RTL written first bends the spec to fit the code: a priority you forgot becomes a row you never test. RTL (register-transfer level: hardware described as registers and the logic between them) written last has nowhere to hide, because the checks already exist and already fail. Write the checks first, and the design has to earn its place.
The design is pulse_counter, an 8-bit counter that watches one input line and counts each rising edge once, holding at 255 instead of wrapping. The listing below is the whole specification you build from, kept as docs/spec.md in both the starter and the reference project.
# pulse_counter specification
Counts rising edges of an input pulse. 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 |
| `pulse_in` | in | 1 | The pulse train to count; each rising edge counts once |
| `clear` | in | 1 | Force the count to zero |
| `count` | out | 8 | Current count. Changes only after a rising edge |
## Behaviour (one row per rising edge, first match wins)
The design also remembers the previous value of `pulse_in` in a register, called `prev` in this table.
`prev` becomes 0 on reset and otherwise takes the value `pulse_in` had at each rising edge.
| `rst_n` | `clear` | Rising edge (`pulse_in` high, `prev` low) | Next `count` |
|---|---|---|---|
| 0 | x | x | 0 (and `prev` to 0) |
| 1 | 1 | x | 0 |
| 1 | 0 | 1 | count + 1, saturating at 255 |
| 1 | 0 | 0 | count (hold) |
## Acceptance criteria
1. Reset to 0 at the next rising edge, from any count, even when `clear` or `pulse_in` is high; reset also returns the remembered previous value to 0.
2. Exactly one count per rising edge of `pulse_in` (previous value 0, current value 1).
3. A pulse held high for several cycles counts once.
4. A falling edge of `pulse_in` counts nothing.
5. `clear` wins over a simultaneous rising edge of `pulse_in`.
6. Saturates at 255: further rising edges leave the count at 255; it does not wrap to 0.
7. Neither `count` nor the remembered value changes between rising edges of `clk`.This listing is the contract that the model, the testbench, and the RTL all answer to.
The figure below lays the steps in the order you run them, top to bottom. Notice the single arrow that runs back up: a red run never moves forward, it returns you to the testbench or the RTL with a failing edge to explain. Trace that loop before you start, because you will walk it several times before the build turns green.
Work the steps in order and finish each one before the next begins.
Read the spec until you can state each criterion as a waveform: what the inputs do on consecutive edges and what the count must be. If criterion 5 puzzles you, the predict box below resolves it before you write anything.
Write the golden model in Python from the table, with a check for every criterion, and run it until it reports its verdict. The model is your executable reading of the spec.
Write the testbench from the same table: a reference model, a cycle task that checks the count before and after each rising edge, directed cases for all seven criteria including 256 pulses for saturation, then a seeded random phase. Watch it fail against the empty starter RTL first. A test that cannot fail proves nothing, as Tests That Can Fail shows.
Write the RTL to satisfy the testbench: the remembered previous value, the priority chain of reset, clear, count, hold, and saturation at 255. Run make all and fix what is red until the loop is green.
Break it on purpose: write three mutants, small wrong versions of your RTL, and confirm the testbench fails on each one. Keep the loop green after every try by restoring your design.
Record the tool versions in tools/versions.md and add the CI (continuous integration: a service that runs your build on every change) workflow, copied from the mini_controller project and pointed at your files. Done means a fresh machine can repeat everything without asking you anything.
You have watched this loop go green already on mini_controller, the 4-bit counter from the earlier parts. The transcript below is its make all, captured from a real run. Your pulse_counter loop ends the same way, with its own name on the verdict line and a nonzero exit standing in for every failure.
# captured terminal output
$ make all 2>&1 | grep -E '^(PASS|iverilog|vvp|verilator|yosys)' | cut -c1-110
verilator --lint-only -Wall --top-module mini_controller rtl/mini_controller.sv
iverilog -g2012 -Wall -s tb_mini_controller -o build/sim.vvp rtl/mini_controller.sv tb/tb_mini_controller.sv
PASS: mini_controller
yosys -Q -T -p 'read_verilog -sv rtl/mini_controller.sv; hierarchy -check -top mini_controller; proc; opt; cheThis output came from Icarus Verilog 13.0 on macOS with the project Makefile. Read it the way the checks will: one verdict line for the simulation, exit status 0 for the passing run, and exit status 2 for the run with the counting bug.
The count returns to 0, and the remembered value becomes 1, because clear outranks counting while the memory still samples the input. The held pulse then counts nothing on the following edges, which is exactly criterion 3 surviving criterion 5.
A green run earns trust only after you have watched the testbench fail. Write three small wrong versions of your own RTL: one that counts a held pulse every cycle, one that checks clear after counting instead of before, and one that wraps 255 to 0. Each breaks exactly one row of the spec table, so each should fail on the directed case for that row. The review rubric in the next lesson gives a point for each mutant killed, up to five, so write two more if you want full marks; a mutant that no input can distinguish from your design earns nothing, so replace it.
Swap each mutant in place of your RTL, run make sim, and confirm the run fails and names the edge. You have already seen the shape of that failure: the last two lines of the transcript above show a counting bug turning a passing run into exit status 2. Restore your RTL after each try and finish with the loop green.
Writing the RTL first and deriving the checks from it. The testbench then repeats your reading of the spec, including its mistakes, and passes on both. Write the model and the checks from the table before the design exists.
Proving saturation with too few pulses. The top hides far away: the count must climb past 255 and stay there, so only the full 256 rising edges prove the point. A short climb passes a design that wraps.
Recording versions from memory instead of the check script. Memory says the tools you meant to install; the script prints the tools you have. Run make check-tools on the machine you claim, and copy what it prints.
Rule: a project is done when a fresh machine can check it without asking you anything.
It proves the checks cannot fail, so the green run means nothing. You rewrite the checks from the spec table, starting with the directed case for the row each mutant breaks, until every mutant fails and the design still passes.
Not necessarily. Rising edges at 255 must hold, so a long sit at the top is correct behavior. The case that separates correct from stuck is clear followed by a fresh pulse: the count must return to 0 and climb again.
Something prints an extra verdict: a second testbench compiled into the run, a leftover debug print, or a copied check that fires twice. Success means exactly one verdict line, so you find the extra one and remove it before calling the project done.
The spec is the only input you trust; the model, the testbench, and the RTL all answer to it.
A green run means the checks passed, and mutant kills mean the checks can fail.
Done means a fresh machine repeats the loop: versions recorded, CI running, one verdict line.