A testbench is the program that drives a hardware design and decides whether what came out was right. In a Verilator flow it is not written in Verilog at all — it is a C++ main() that pokes the model’s input ports, calls eval() to advance the compiled circuit, and compares the output ports against an answer computed in software (Verilator connecting guide). That framing matters more than it sounds: because the checker is ordinary C++, the testbench can hold a golden reference model in memory and compare against it every single cycle, which is the technique that scales from an eight-bit counter to a five-stage RISC-V pipeline. RTL verification is the discipline built on top of that primitive — a hierarchy that runs from directed tests you write by hand, through an official conformance suite such as The riscv-tests Suite, to differential testing against a known-good implementation. The rule that organises all of it is simple and unforgiving: a test that requires a human to look at a waveform to decide whether it passed does not scale, and therefore is not a test. Waveforms are for diagnosing a failure you have already detected automatically (Waveform Debugging) — never for detecting it.
This note is about the practice. The tool itself — what Verilator is, how it compiles RTL to C++, its two-state semantics, its language coverage and its release history — is covered in Verilator and is not repeated here. Every command line, every log line and every measurement below was produced on Verilator 5.046 2026-02-28 rev fedora-5.046, Icarus Verilog 13.0, GTKWave 3.3.127, Surfer 0.7.0, clang 22.1.8 targeting riscv32, and riscv64-linux-gnu-gcc 16.1.1, on an AMD Ryzen AI MAX+ 395 (32 threads), Fedora 44.
Mental Model
A hardware module is not a function you can call. It has no entry point and no return value; it is a lump of state and combinational logic that reacts to a clock. To exercise it you have to build the world around it — supply the clock, supply the reset, supply the inputs at the right moment relative to the clock, and observe the outputs at the right moment too. That surrounding world is the testbench, and in the vocabulary of the field the module being exercised is the DUT (Device Under Test), sometimes UUT (Unit Under Test).
The mental model that makes everything else fall into place is: the testbench is a program, the DUT is a data structure that program mutates, and one clock cycle is a handful of function calls — two at minimum (raise the clock, lower it), three when you settle the inputs first. Verilator compiles the module into a C++ class whose public members are the top module’s ports; the testbench assigns to the input members, calls eval(), and reads the output members. Nothing about it is magic, and — importantly — nothing about it is Verilog. The whole apparatus of stimulus generation, checking, logging and file I/O is written in a language with a debugger, a package manager, and printf.
flowchart LR
subgraph TB["testbench — C++ main()"]
CLKGEN["clock generator<br/>clk = !clk<br/>timeInc(period/2)"]
RSTSEQ["reset sequencer<br/>assert N cycles<br/>deassert while clk low"]
STIM["stimulus source<br/>directed vectors ·<br/>a compiled program ·<br/>seeded random"]
REF["reference model<br/>the same answer,<br/>computed in software"]
CHK{"checker<br/>dut_out == ref_out ?"}
TRACE["tracer<br/>tfp.dump(time)"]
end
subgraph DUTBOX["DUT — the compiled RTL model"]
PORTS["input ports<br/>clk · rst · data"]
LOGIC["always_ff / always_comb<br/>compiled to C++"]
OUT["output ports"]
PORTS --> LOGIC --> OUT
end
CLKGEN --> PORTS
RSTSEQ --> PORTS
STIM --> PORTS
STIM --> REF
OUT --> CHK
REF --> CHK
CHK -->|"pass"| NEXT["next cycle"]
CHK -->|"fail"| REPORT["print cycle, time,<br/>expected, actual<br/>· exit non-zero"]
LOGIC -.->|"every signal,<br/>every timestamp"| TRACE
TRACE --> VCD["trace.vcd / trace.fst"]
The anatomy of a testbench. What it shows: five distinct jobs — generate the clock, sequence the reset, produce stimulus, compute the expected answer independently, and compare — plus a sixth (tracing) that runs alongside and is used only after a comparison has already failed. The insight to take: the reference model and the checker are what make this a test; without them you have a stimulus generator that produces a waveform, and a waveform is not a verdict. Notice too that the stimulus feeds both the DUT and the reference — that shared input is the entire basis of differential testing, and it is why the reference must be an independent implementation rather than a copy of the DUT’s logic.
The second thing to internalise is that the testbench’s notion of time is a bookkeeping counter, not a physical quantity. Verilator’s VerilatedContext holds a 64-bit simulation time that only ever advances because you called timeInc(). The compiled model does not consume time; a call to eval() is instantaneous in simulated time and takes however many nanoseconds of wall-clock the host CPU needs. Simulated time exists for exactly two purposes: to stamp entries in the waveform file, and to give $time in the RTL something to print. If you never trace and never print time, you can omit timeInc() entirely and the design will behave identically. Beginners routinely believe simulated time is driving the design; it is not. The clock signal drives the design, and the clock signal is a variable you toggle by hand.
The Generated Model — What Verilator Hands You
Start with the design the definitely-not-esp32 MOC names as the Stage 0 program: a module that does nothing but count. Here it is, with an enable and a wrap flag so there is more than one signal to look at:
// counter.v -- Stage 0: "a module that does nothing but count".module counter #( parameter WIDTH = 8) ( input wire clk, input wire rst, // synchronous, ACTIVE HIGH input wire en, output reg [WIDTH-1:0] count, output wire wrapped // high on the cycle count returns to 0); assign wrapped = (count == {WIDTH{1'b1}}) & en; always @(posedge clk) begin if (rst) count <= {WIDTH{1'b0}}; else if (en) count <= count + 1'b1; endendmodule
Line by line: WIDTH is a parameter, so the same source elaborates to an 8-bit or a 32-bit counter; rst is documented in a comment as active high and synchronous, which is a decision, not a default, and one the testbench must agree with; wrapped is a continuous assignment, so it is combinational — it changes the instant count or en changes, with no clock involved; and the always @(posedge clk) block is the only sequential logic, using non-blocking assignment (<=) so that all flip-flops sample their inputs before any of them update.
Verilating it produces a C++ class. The command is:
--cc requests a C++ (rather than SystemC) model; --exe says a user main() is being supplied so an executable should be produced; --build tells Verilator to run make itself rather than leaving a Makefile for you; --Mdir names the output directory; --top-module disambiguates when a file holds several modules. --trace requests waveform instrumentation. Verilator reported the work it did:
- V e r i l a t i o n R e p o r t: Verilator 5.046 2026-02-28 rev fedora-5.046
- Verilator: Built from 0.026 MB sources in 2 modules, into 0.038 MB in 8 C++ files needing 0.000 MB
- Verilator: Walltime 2.708 s (elab=0.000, cvt=0.003, bld=2.701); cpu 0.007 s on 4 threads; allocated 37.340 MB
Note the breakdown: elaboration and conversion took 3 milliseconds; the C++ build took 2.7 seconds. For a design this size, Verilator is not the bottleneck — g++ is. That ratio holds up to surprisingly large designs and is why the edit-compile-run loop for a small core stays in the seconds.
The generated class exposes the ports as plain public data members. A 1-bit port becomes CData (a uint8_t), up to 32 bits IData (uint32_t), up to 64 bits QData, and wider signals become VlWide arrays. The consequence is that a testbench reads and writes hardware signals as if they were struct fields:
Vcounter dut{&ctx};dut.rst = 1; // drive an input portdut.eval(); // let the model reactprintf("%u\n", dut.count); // read an output port
Only top-level ports are directly accessible
Internal signals — count inside a submodule, a pipeline register three levels down — are not public members. Verilator may have optimised them away entirely. To read one from C++ you must either promote it to a top-level output, mark it with the /* verilator public */ or /* verilator public_flat_rd */ attribute, or reach it through the VPI. This is not a limitation of the waveform trace, which sees far more than the C++ API does; it is one of the reasons waveform debugging and printf debugging are complementary rather than redundant.
Driving the Clock — eval(), timeInc(), and One Simulated Cycle
eval() is the whole simulation engine, and understanding precisely what it does is the difference between a testbench that works and one that mysteriously reports values one cycle out. The Verilator manual states the order of operations explicitly:
When eval() (or eval_step()) is called Verilator looks for changes in clock signals and evaluates related sequential always blocks, such as computing always_ff @(posedge…) outputs. […] Then Verilator evaluates combinational logic.
Note combinatorial logic is not computed before sequential always blocks are computed (for speed reasons). Therefore it is best to set any non-clock inputs up with a separate eval() call before changing clocks. (Verilator connecting guide)
Unpack that. eval() does not simulate a time interval. It compares each clock signal’s current value against the value it had at the previous eval(), and where it sees a rising edge it runs the sequential blocks sensitive to that edge. Then, and only then, it settles the combinational logic. Everything that happens is triggered by your assignment to the clock variable between the two calls.
sequenceDiagram
autonumber
participant TB as "testbench (C++)"
participant CTX as VerilatedContext
participant M as "compiled model"
participant T as tracer
Note over TB,T: one simulated clock cycle = four testbench actions
TB->>M: set non-clock inputs — dut.a, dut.b
TB->>M: eval() — settle combinational only, no clock edge seen
M-->>TB: combinational outputs now valid
TB->>CTX: timeInc(half_period)
TB->>T: dump(ctx.time()) — stimulus visible BEFORE the edge
TB->>M: dut.clk = 1
TB->>M: eval() — RISING EDGE detected
M->>M: run always_ff blocks, flops capture inputs
M->>M: settle combinational from new flop values
M-->>TB: registered outputs now hold this cycle's result
TB->>CTX: timeInc(half_period)
TB->>T: dump(ctx.time())
TB->>M: dut.clk = 0
TB->>M: eval() — falling edge, nothing is sensitive to it
TB->>CTX: timeInc(half_period)
TB->>T: dump(ctx.time())
Note over TB,M: the checker compares dut outputs against the reference here
One eval() cycle in Verilator, step by step. What it shows: the four eval() calls that make up a cycle and what each one is actually for — the first settles inputs so the design sees them before the edge; the second is where all state changes happen; the third and fourth exist only to complete the clock waveform for the trace. The insight to take: step 2 is the one beginners omit, and the manual singles it out. Omitting it does not usually change the DUT’s behaviour (a flop reads the input value present at the moment eval() sees the edge, whether or not there was an earlier settling call) — but it does change what the trace shows, because a stimulus change that is never dumped at its own timestamp appears in the waveform simultaneously with the clock edge, which is precisely the ambiguity that makes a waveform unreadable.
Here is that cycle as real code, from the counter testbench:
auto step = [&](int dt) { ctx.timeInc(dt); dut.eval(); tfp.dump(ctx.time()); };// ... clk is currently low, time T, already dumpeddut.a = stimulus; // apply non-clock inputsstep(2); // settle + dump at T+2 (setup)dut.clk = 1; step(3); // rising edge at T+5dut.clk = 0; step(5); // falling edge at T+10
Three things about this idiom are worth calling out because they are the source of most first-week confusion.
The timescale is 1 ps by default. Verilator’s manual says the default timeunit/timeprecision when no `timescale directive is present is 1ps/1ps, “to match SystemC” (Verilator argument reference). This is directly visible in the VCD produced by the counter run:
$version Generated by VerilatedVcd $end
$timescale 1ps $end
So timeInc(5) is five picoseconds, and a 10-unit period is a 100 GHz clock. Nothing cares — simulated time is bookkeeping — but a waveform viewer will label the axis in picoseconds and you should not be surprised. Pass --timescale 1ns/1ps if you want the numbers to read like a real clock.
Every dump() must land on a distinct timestamp. An early draft of the differential testbench below called dump() twice at the same simulated time; Verilator’s tracer refuses and says so, once per occurrence:
%Warning: previous dump at t=25, requesting t=25, dump call ignored
The trace is not corrupted — the second dump is simply dropped — but the value change you were trying to record is lost, so the waveform silently disagrees with the printouts. The fix is arithmetic, not API: choose a half-period large enough that stimulus, rising edge and falling edge each get their own instant. The step(2)/step(3)/step(5) split above exists for exactly this reason.
--main and --binary exist if you want the loop written for you.--binary is documented as an alias for --main --exe --build --timing (Verilator argument reference), which generates a main() and enables timing constructs, so a self-contained Verilog testbench with initial, always #5 clk = ~clk; and $finish runs directly:
$ verilator --binary --trace-vcd -j 8 tb_self.v --top-module tb_self -o Vtb_self$ ./obj/Vtb_selfresult=98- tb_self.v:25: Verilog $finish- S i m u l a t i o n R e p o r t: Verilator 5.046 2026-02-28- Verilator: $finish at 100ps; walltime 0.000 s; speed 1.202 us/s
That is a genuinely useful mode for a quick experiment or for running a testbench that must also work under Icarus Verilog. It is the wrong mode for a CPU project, because it puts the checker back inside Verilog, where you cannot easily hold a reference model, read an ELF file, or emulate a UART. The C++ testbench is the one that scales.
Reset Sequencing, and the First Bug Everybody Writes
Reset is where the first real bug lives, and it is worth a fully worked example because the failure is silent, systematic, and looks like a design bug when it is a testbench bug.
A synchronous reset is a synchronous input: it only does anything at a clock edge. So the sequence a testbench must produce is (1) drive reset to its active level, (2) provide at least one — conventionally several — clock edges while it is active, (3) drive it inactive while the clock is low, and (4) start counting cycles. Step 3 is the one that goes wrong. Here is the correct version from sim_main.cpp:
// --- reset sequence --------------------------------------------------- dut.clk = 0; dut.rst = 1; dut.en = 0; dut.eval(); tfp.dump(ctx.time()); ctx.timeInc(5); // settle inputs at t=0 for (int i = 0; i < 2; i++) { // 2 full clocks in reset dut.clk = 1; dut.eval(); tfp.dump(ctx.time()); ctx.timeInc(5); dut.clk = 0; dut.eval(); tfp.dump(ctx.time()); ctx.timeInc(5); } dut.rst = 0; dut.en = 1; dut.eval(); tfp.dump(ctx.time()); // inputs visible before edge
and here is the buggy version, which differs by the placement of one line:
dut.en = 1; // enable asserted... // BUG: dut.rst = 0 belongs HERE, before the first counting edge. for (int cycle = 0; cycle < 300; cycle++) { ctx.timeInc(5); dut.clk = 1; dut.eval(); tfp.dump(ctx.time()); dut.rst = 0; // ...but reset is only dropped AFTER the edge ...
Both testbenches hold reset for two clocks. Both deassert it. The buggy one deasserts it after the first counting edge instead of before, so the design spends one extra edge in reset. Run them:
300 mismatches out of 300 cycles, and the RTL is byte-for-byte identical in both runs. This is the signature of a reset bug: not an occasional wrong value but a permanent, constant offset, present from the very first checked cycle and never self-correcting. If your very first cycle is wrong and every subsequent cycle is wrong by the same amount, suspect the reset sequence before you suspect the design.
The two VCD files, rendered side by side (only the first 90 ps of each, and only the top-level signals), show the divergence exactly:
CORRECT DIVERGENCE
time 0 5 10 15 20 25 30 35 40 45 50 |
clk 0 1 0 1 0 0 1 0 1 0 1 |
rst 1 1 1 1 1 0 0 0 0 0 0 v
en 0 0 0 0 0 1 1 1 1 1 1
count 0 0 0 0 0 0 1 <- 1 2 2 3 first increment at t=30
^
`-- reset released HERE, while clk is low
BUGGY
time 0 5 10 15 20 30 35 40 45 50 55
clk 0 1 0 1 0 1 0 1 0 1 0
rst 1 1 1 1 1 1 <- still asserted at the edge!
en 0 0 0 0 0 1 1 1 1 1 1
count 0 0 0 0 0 0 0 1 2 2 3 first increment at t=40
^
`-- DIVERGENCE: count should be 1 here
ASCII waveform of the reset bug, transcribed directly from counter.vcd and counter_bad_reset.vcd. Mermaid has no timing-diagram type that renders in Obsidian, so this uses the vault’s sanctioned ASCII fallback (see the Diagrams section of the vault conventions); the values are real VCD data, extracted by a small VCD parser, not hand-drawn. What it shows: the correct trace has an extra sample at t=25 — the settling eval() after rst and en change — and count first increments at t=30. The buggy trace has no sample at t=25 at all, because no eval()/dump() happened between the input change and the clock edge, so rst is still 1 when the edge arrives and the first increment slips to t=40. The insight to take: the missing t=25 column is itself the diagnosis. When a stimulus change and a clock edge share a timestamp in the waveform, you cannot tell which the flop saw — and that ambiguity is what the “separate eval() before changing clocks” rule exists to remove.
Four rules follow from this, and they are worth writing on the wall:
Assert reset before the first eval(), not after. Two-state Verilator zero-fills every flip-flop at construction, so a design with no reset at all appears to work. That masking is discussed under Failure Modes below; it means a working simulation is not evidence that your reset is correct.
Hold reset for several clocks, not one. One edge is enough for a purely synchronous reset in simulation, but real designs contain reset synchronisers and start-up FSMs that need more, and holding longer costs nothing.
Deassert while the clock is at its inactive level. For a posedge design that means deassert with clk == 0, then eval(), then produce the edge. This is the direct analogue of meeting setup time on real silicon.
Make the polarity impossible to get wrong. Name the port rst_n if it is active-low and rst if it is active-high, and say so in a comment on the port. A polarity mismatch between RTL and testbench produces a design that is either permanently held in reset (obvious) or never reset at all (invisible under two-state).
Measured, not assumed — asynchronous reset and eval()
A reset pulse that begins and ends between two eval() calls is invisible to Verilator, even on an always @(posedge clk or negedge rst_n) block. Measured on Verilator 5.046 with an 8-bit counter using an asynchronous active-low reset:
after 10 cycles count=10after invisible reset pulse count=10 (0 => pulse was seen)after eval-separated pulse count=0 (0 => pulse was seen)
The first pulse — rst_n = 0; rst_n = 1; eval(); — left the counter at 10; the second — rst_n = 0; eval(); rst_n = 1; eval(); — reset it to 0. This is the direct consequence of the documented evaluation model: eval() detects edges by comparing each signal against its value at the previous call, so any transition that is undone before the next call never existed. The practical rule is that an eval() is the simulation’s clock tick for every edge-sensitive signal, not just for clk — if you want the design to see a pulse, you must call eval() while it is asserted.
Self-Checking Testbenches
The distinction that matters most in this whole note is between a testbench that produces output and one that produces a verdict. The first prints values or dumps a waveform and leaves a human to decide; the second computes the expected answer itself, compares, and exits with a status code. Only the second can be run by a script, run on every commit, or run five hundred times across a regression suite.
The counter testbench is self-checking, and the mechanism is three lines:
unsigned expect = 0; // the reference model: a C++ variable int errors = 0; for (int cycle = 0; cycle < 300; cycle++) { ctx.timeInc(5); dut.clk = 1; dut.eval(); tfp.dump(ctx.time()); // rising edge: count updates expect = (expect + 1) & 0xff; // golden model, in C++ if (dut.count != expect) { if (errors++ < 5) printf("MISMATCH cycle %3d t=%lu: dut.count=%3u expected=%3u\n", cycle, (unsigned long)ctx.time(), dut.count, expect); } ... } printf("%s: %d cycles, %d mismatches\n", errors ? "FAIL" : "PASS", 300, errors); return errors != 0;
Every element of that is deliberate:
The reference is an independent implementation.expect = (expect + 1) & 0xff is not a copy of the RTL; it is the specification of an 8-bit wrapping counter, written in a different language, by (notionally) a different route. If you compute the expected value by reading it out of the DUT, you have written a tautology.
The check runs every cycle, not at the end. Checking only the final value tells you that something is wrong; checking every cycle tells you when, which is the single most valuable fact for the Waveform Debugging step that follows.
The failure message carries the cycle number and the simulated time. The cycle number is what you reason with; the simulated time is what you type into the waveform viewer’s cursor box. Printing one without the other doubles the work.
Errors are capped.if (errors++ < 5) prints the first five and counts the rest. A systematic bug produces one failure per cycle; without a cap a 300-cycle run floods the terminal and a 10-million-cycle run fills the disk. The first failure is almost always the only one you need.
The exit status is the verdict.return errors != 0 is what lets make test or a CI job fail. A testbench that always returns 0 is decorative.
Wrapping the whole thing so that a script can drive it, and so that the counter’s wrapped output is checked too, the pattern generalises to a small structure that every subsequent testbench in the project reuses: a tick() helper, a check(name, got, want) helper that increments a global error count and prints uniformly, and a finish() that prints PASS/FAIL and returns the status. It is worth building this once, early, because from Stage 2 onwards every core testbench is this shape with a bigger reference model bolted on.
Checking style
Detects a bug?
Localises it?
Scales to 10⁶ cycles?
When it is the right tool
Eyeball the waveform
Only if you look at the right signal at the right time
Yes, superbly
No
Diagnosing a failure a checker already found
$display/printf trace, read by a human
Sometimes
Roughly
No
First bring-up of a brand-new module
Final-value check
Yes, for that one value
No
Yes
Smoke test; riscv-tests pass/fail signalling
Per-cycle self-check against a software model
Yes
To the exact cycle
Yes
The default for everything in this project
Differential against an independent implementation
Yes, including bugs you did not anticipate
To the exact cycle
Yes
Validating a pipeline against a single-cycle core
Concurrent assertions in the RTL
Yes, for the property asserted
To the exact cycle and the exact property
Yes
Invariants that must hold everywhere, e.g. one-hot state
Checking strategies ranked by what they can actually do. What it shows: the two columns that matter are “localises it” and “scales” — and only the bottom three rows have both. The insight to take: the top two rows are not tests, they are observations. They belong in a debugging session, not in a regression suite. Every hour spent turning a row-1 workflow into a row-4 workflow is repaid the first time a change breaks something you were not looking at.
Assertions
An assertion moves the check inside the design. Instead of the testbench watching an output port, a statement in the RTL declares a property that must hold, and the simulator fires if it does not. This is powerful for two reasons: the property is written next to the logic it constrains, so it stays correct when the logic is refactored; and it is checked on every stimulus, including stimulus from tests written later by someone who never heard of the invariant.
SystemVerilog defines two families. An immediate assertion is a procedural statement — assert (expr); inside an always block — evaluated like an if. A concurrent assertion is declared with assert property (...) and is clocked: it describes behaviour over time using the sequence and property language, with operators such as |-> (overlapping implication), |=> (non-overlapping implication, “on the next cycle”), $past, ##N (delay), and disable iff (a reset guard).
Verilator supports immediate assertions fully, and a useful subset of concurrent assertions — enough for one-cycle implications and $past comparisons, but not the full property language with SEREs. Assertion checking is off by default and enabled with --assert. Here is a module with three concurrent assertions and one cover point, all of which Verilator 5.046 accepted:
module counter_sva #(parameter WIDTH = 8) ( input logic clk, input logic rst, input logic en, output logic [WIDTH-1:0] count); always_ff @(posedge clk) begin if (rst) count <= '0; else if (en) count <= count + 1'b1; end // Concurrent assertion: the property Verilator does support -- // a simple one-cycle implication with $past. property p_hold_when_idle; @(posedge clk) disable iff (rst) (!en) |=> (count == $past(count)); endproperty a_hold_when_idle: assert property (p_hold_when_idle) else $error("count changed at t=%0t while en was low", $time); // A deliberately FALSE property, to see what a firing assertion prints. a_never_eight: assert property (@(posedge clk) disable iff (rst) count != 8'd8) else $error("count reached 8 at t=%0t", $time); // Functional cover point. c_wrap: cover property (@(posedge clk) disable iff (rst) count == 8'hFF);endmodule
Reading the first property symbol by symbol: @(posedge clk) fixes the sampling clock; disable iff (rst) suppresses the check whenever reset is active, which is essential because reset legitimately violates almost every steady-state invariant; (!en) is the antecedent; |=> means “then, starting one clock later”; and (count == $past(count)) is the consequent, where $past(count) is the value count held at the previous sampling edge. In English: whenever the enable is low, the count must be unchanged on the following cycle.
Built with --assert and run, the deliberately-false property fires:
Three details in that output pay for the whole mechanism. [89] is the simulated time at which the property failed — paste it straight into a waveform viewer’s cursor. TOP.counter_sva.a_never_eight is the full hierarchical path and the label you gave the assertion, which is why labelling assertions is not optional. And the run aborts with a non-zero exit status: a failing assertion stops the simulation at the first violation rather than letting it run on into a cascade of derived failures, which is exactly what you want when hunting a first divergence.
Label every assertion, and always write the else $error(...)
Without a label, the message names an auto-generated identifier that tells you nothing. Without the else clause you get Verilator’s generic text and no values. The two together turn an assertion from “something broke” into “count changed at t=89 while en was low”, which is a diagnosis.
SystemVerilog assertion construct
Verilator 5.046
Use it for
assert (expr); (immediate, in a procedural block)
Supported
Cheap sanity checks inside always blocks
assume / cover (immediate)
Supported
Constraining and counting
assert property (@(posedge clk) expr)
Supported
“This must always be true at every edge”
disable iff (rst)
Supported
Suppressing checks during reset — essential
|=> and |-> implication with a simple consequent
Supported
One-cycle cause/effect properties
$past(sig)
Supported
“Compare against last cycle”
cover property (...)
Supported, reported via --coverage-user
Functional coverage points
Multi-cycle sequences — ##N on either side of an implication
Not supported — %Error-UNSUPPORTED: Implication with sequence expression
Protocol-shaped properties — write a C++ scoreboard instead
throughout, within, [*N:M]
Not supported — each named individually in the error
As above
Local variables inside sequences
Not supported
Data-tracking properties
Full SERE property language / UVM checkers
Not supported
Commercial verification IP
What Verilator’s assertion support does and does not cover, measured on 5.046 by linting each construct in turn (verilator --lint-only --assert). What it shows: the supported column is exactly the “one-cycle invariant” family, and the unsupported column is exactly the “behaviour over a window” family. The insight to take: that split is not arbitrary — a one-cycle property is a boolean over the current and previous sampled state, which a compiled two-state model can evaluate for free, whereas a multi-cycle sequence needs a matching engine. When you want a multi-cycle property under Verilator, encode it as a small state machine in the RTL and assert a one-cycle invariant on that machine.
The unsupported rows above are not inferred from documentation; each was linted and the exact rejection recorded. For example:
$ verilator --lint-only --assert m3.sv --top-module m3%Error-UNSUPPORTED: m3.sv:3:67: Unsupported: Implication with sequence expression 3 | a_seq2: assert property (@(posedge clk) disable iff (rst) req |=> ##1 ack); | ^~~%Error: Exiting due to 1 error(s)$ verilator --lint-only --assert m.sv --top-module m%Error-UNSUPPORTED: m.sv:6:90: Unsupported: [*] boolean abbrev expression%Error-UNSUPPORTED: m.sv:6:92: Unsupported: boolean abbrev (in sequence expression)%Error-UNSUPPORTED: m.sv:6:76: Unsupported: throughout (in sequence expression)
Note the failure mode is a hard elaboration error, not silent acceptance — Verilator will not quietly ignore a property it cannot check, which is the right behaviour and worth relying on.
What Verilator does not do. The full IEEE 1800 property language — multi-cycle sequences, throughout, within, intersect, local variables in sequences, and the checker/bind machinery used by commercial verification IP — is outside Verilator’s supported subset (see Verilator for the full language-coverage picture). For a small core this is barely a constraint: the invariants worth asserting are things like the register file never writes to x0, the program counter is always 4-byte aligned unless the C extension is enabled, exactly one bus slave is selected, and a pipeline stall never coincides with a flush — all of which are one-cycle properties expressible in the supported subset.
Golden-Reference and Differential Testing
This is the technique that carries the project from Stage 3 onward, and the definitely-not-esp32 MOC states the plan explicitly: “A single-cycle core is not a stepping stone you throw away — it is the reference model you will compare the pipelined version against for the rest of the project.”The Single-Cycle Processor is deliberately built first, is deliberately slow, and is deliberately obvious, because its whole later purpose is to be the thing that is right.
Differential testing (also called co-simulation, or ISS lockstep when the reference is an instruction-set simulator) works like this: feed identical stimulus to two implementations, align their outputs in time, and compare every cycle. Any disagreement is a bug in one of them — and because the reference is the simple one, it is almost always a bug in the fast one.
flowchart TB
STIM["stimulus<br/>same vectors,<br/>fixed seed"]
subgraph REFBOX["reference — obviously correct"]
REF["single-cycle datapath<br/>(combinational)<br/>or a software ISS"]
end
subgraph DUTBOX["DUT — fast, and therefore suspect"]
DUT["pipelined datapath<br/>(N registered stages)"]
end
STIM --> REF
STIM --> DUT
REF --> Q["FIFO delay line<br/>depth = pipeline latency"]
Q --> CMP{"compare<br/>every cycle"}
DUT --> CMP
CMP -->|"equal"| CONT["continue"]
CMP -->|"differ"| STOP["record cycle, time,<br/>both values, the stimulus<br/>· stop · open the trace"]
The differential-testing harness. What it shows: the FIFO between the reference and the comparator is the entire trick — the pipelined DUT produces the answer to cycle n’s stimulus several cycles later, so the reference’s answer must be delayed by exactly the same latency before comparison. The insight to take: getting that depth wrong produces a testbench that fails on a correct design, which is the most demoralising possible failure mode. Determine the latency once, from the RTL, and assert it — do not tune it until the test passes.
Here is a real, runnable instance of that harness, small enough to read in full. Two ALUs: alu_single is purely combinational — the reference — and alu_pipe is a two-stage version that registers its operands, computes, and registers the result. A parameter plants a defect:
module alu_pipe #(parameter BUG = 0) ( input wire clk, input wire rst, input wire [31:0] a, input wire [31:0] b, input wire [2:0] op, output reg [31:0] y); reg [31:0] a_q, b_q; reg [2:0] op_q; wire [31:0] b_s2 = (BUG != 0) ? b : b_q; // <-- the planted defect wire [31:0] y_comb; alu_single u_alu (.a(a_q), .b(b_s2), .op(op_q), .y(y_comb)); always @(posedge clk) begin if (rst) begin a_q <= 32'd0; b_q <= 32'd0; op_q <= 3'd0; y <= 32'd0; end else begin a_q <= a; b_q <= b; op_q <= op; y <= y_comb; end endendmodule
With BUG=0, stage 2 reads b_q, the registered copy of b. With BUG=1 it reads the input port b directly — so stage 2 combines this cycle’s b with last cycle’s a. This is an operand-skew bug, and it is not a strawman: forgetting to pipeline one member of a bundle is among the most common real errors when a single-cycle datapath is cut into stages, and it is exactly the class of mistake Pipeline Hazards and Operand Forwarding machinery is built to avoid.
The testbench drives both from the same random() stream with a fixed seed, delays the reference through a std::deque, and compares:
std::deque<unsigned> refq; // reference outputs awaiting the pipe latency srandom(1); // fixed seed -> the run is reproducible for (int cycle = 0; cycle < N; cycle++) { dut.a = (unsigned)random(); dut.b = (unsigned)(random() % 40); dut.op = (unsigned)(random() % 8); step(cycle == 0 ? 1 : 2); // settle the combinational reference refq.push_back(dut.ref_y); // sample the golden answer for THIS stimulus dut.clk = 1; step(3); // rising edge dut.clk = 0; step(5); // falling edge if (refq.size() > 1) { // pipeline latency at y is one cycle unsigned expect = refq.front(); refq.pop_front(); if (dut.dut_y != expect) { /* report cycle, time, both values */ } } }
Building the same sources twice, with -GBUG=0 and -GBUG=1 — -G<name>=<value> overrides a top-level parameter from the command line, which is the clean way to get two variants without editing source — gives:
Read the numbers carefully, because the interesting one is not 1631. It is 1631 out of 2000 — 81.5%. The bug is not deterministic from the outside: in 18.5% of cycles the operation happened to be insensitive to the skew (an AND where the differing bits were already zero, a shift where both b values landed in the same range, or the rare cycle where consecutive b values collided). A design with an 18.5% pass rate per cycle is a design that a short directed test can easily miss entirely. Notice also that cycle 2 is absent from the list — a correct result in the middle of a systematically broken run. If you had written three directed vectors and one of them was cycle 2, you would have shipped the bug.
That is the argument for differential testing in one paragraph: it tests every cycle against an independent oracle, so it catches bugs whose triggering condition you did not think of. Directed tests can only find bugs you anticipated well enough to write a vector for.
Two practical notes on scaling this to a CPU. First, the comparison point should be architectural state at instruction retirement, not every internal wire: the pipelined core and the single-cycle core have completely different internals, and only the committed register file, the program counter, and memory writes are required to agree. Second, when the DUT is a full core, the reference does not have to be RTL at all — a software instruction-set simulator works, and the RISC-V ecosystem provides several. The sail-riscv model is the formal specification adopted by RISC-V International and generates an executable emulator from the same source that generates the documentation and the theorem-prover definitions, which makes it about as authoritative a reference as exists. riscv-tests itself anticipates this workflow: each test’s data section “will be captured at the end of the test to act as a signature from the test. The signature can be compared with that from a run on the golden model” (riscv-tests README).
Coverage, and What It Does Not Tell You
Coverage answers a question the pass/fail result cannot: did my tests actually exercise the design? A suite of 500 tests that all pass is worthless if they collectively never take a branch, never fill a queue, and never assert an interrupt. Verilator instruments the model to count how often each construct was reached and writes the counts to a data file.
--coverage is documented as an alias enabling all forms — --coverage-line, --coverage-toggle, --coverage-expr, --coverage-fsm and --coverage-user (Verilator argument reference). The four that matter for a small design are:
Metric
Flag
What it counts
What it misses
Line
--coverage-line
Times each basic block was entered
A line executed once with the wrong data
Toggle
--coverage-toggle
Each signal bit going 0→1 and 1→0
Bits that toggle but never in the combination that matters
Expression
--coverage-expr
Which sub-term combinations of a condition occurred
Anything outside the enumerated permutations (default max 32)
Functional / user
--coverage-user
cover property / covergroup points you wrote by hand
Everything you did not think to write a cover point for
The counts are collected at runtime and must be written explicitly by the testbench — this is the step that silently produces nothing if omitted:
Running the counter for 20 cycles with --assert --coverage produced a 38-line coverage.dat whose records are self-describing:
# SystemC::Coverage-3
C 'fassertcov/counter_sva.svl13n5tlinepagev_line/counter_svaoblockS13hTOP.counter_sva' 22
C 'fassertcov/counter_sva.svl14n18texprpagev_expr/counter_svao(en==0) => 0hTOP.counter_sva' 2
C 'fassertcov/counter_sva.svl14n18texprpagev_expr/counter_svao(rst==0 && en==1) => 1hTOP.counter_sva' 20
C 'fassertcov/counter_sva.svl14n18texprpagev_expr/counter_svao(rst==1) => 0hTOP.counter_sva' 2
C 'fassertcov/counter_sva.svl2n30ttogglepagev_toggle/counter_svaoclk:0->1hTOP.counter_sva' 22
The tagged fields are f=file, l=line, n=column, t=type, page, o=comment/expression text, h=hierarchy, and the trailing integer is the hit count. verilator_coverage turns that into a summary and an annotated source listing:
$ verilator_coverage --annotate cov_ann --annotate-min 1 coverage.datTotal coverage (6/13) 46.00%See lines with '%00' in cov_ann
The %000000 markers are the whole point. Two of them are genuinely informative. c_wrap never fired because the test ran the counter to 20, not to 255 — the wrap case, which is where an off-by-one in the wrap logic would live, was never tested. And p_hold_when_idle never evaluated because en was tied high after reset — an assertion that never runs is not protecting anything, and coverage is the only thing that would have told you.
And now the limits, which are more important than the metrics. 46% line-and-toggle coverage on a 20-cycle run of a counter tells you almost nothing about correctness, and 100% would tell you only slightly more. Structural coverage measures reachability, not correctness:
100% line coverage is compatible with a completely broken design. Every line of the operand-skew ALU above executes on every cycle. Line coverage on the buggy BUG=1 build is identical to the correct build; it is the differential check, not the coverage number, that finds the defect.
Toggle coverage is easy to game and easy to satisfy accidentally. Feeding random data to a 32-bit datapath toggles every bit within a few dozen cycles while testing nothing about the operations.
Coverage cannot cover what you did not write. A missing case in a case statement with a default is fully covered and completely wrong.
The useful number is functional coverage, and functional coverage is only as good as the cover points a human thought to write. That is a fundamentally different activity from running a tool.
The honest role of coverage in a small project is as a gap-finder, not as a score. Run it once after the directed tests and once after the official suite, read the %000000 lines, and ask “why did this never happen?” for each one. Chasing the percentage upward is a well-documented way to write tests that improve the metric and find nothing.
Constrained-Random Stimulus, and Why It Is Usually Overkill Here
Constrained-random verification is the methodology that dominates commercial ASIC work. Instead of writing vectors, you declare a transaction class with random fields and a set of constraint blocks that restrict them to legal combinations, then let a solver generate thousands of legal-but-unexpected stimuli. Coverage points tell you which corners have been hit; a coverage-driven loop adjusts the constraints to chase the rest. The full apparatus — classes, randomize(), covergroups, virtual interfaces, factories, sequencers — is the Universal Verification Methodology (UVM).
For a RISC-V core specifically, the mature tool is riscv-dv, a “SV/UVM based open-source instruction generator for RISC-V processor verification” supporting RV32IMAFDC and RV64IMAFDC, machine/supervisor/user modes, page-table randomisation, privileged-CSR randomisation, illegal-instruction generation, and “co-simulation with multiple ISS: spike, riscv-ovpsim, whisper, sail-riscv” (riscv-dv README). That last line is the point: the generator is only half of it — the other half is differential comparison against a reference simulator, which is the same technique described above, industrialised.
And it is usually the wrong first investment for a project at this stage, for four concrete reasons.
The tooling is not free here.riscv-dv’s own prerequisites say it needs “an RTL simulator which supports SystemVerilog and UVM 1.2” and that it has been verified with VCS, Xcelium, Questa and Riviera-PRO — all commercial. Verilator’s class and randomisation support has been growing through the 5.x line but is not a drop-in UVM host (see Verilator’s language-coverage section). Adopting the methodology means adopting a licensed simulator or fighting the tool.
Random stimulus needs a reference to be useful, and the reference is the expensive part. Given a golden model, random stimulus is nearly free — the twenty lines of random() in the differential ALU testbench above are constrained-random stimulus, with the constraints expressed as random() % 40 and random() % 8. Without a golden model, random stimulus produces waveforms nobody can check.
Directed tests find the first 90% of bugs faster. Early in bring-up almost everything is broken, and a hand-written vector that isolates one instruction tells you far more than a random program that fails for six reasons at once. Randomisation earns its keep when the obvious bugs are gone and you need to find the ones nobody imagined.
riscv-tests is already a large body of expert-designed directed stimulus, free, and targeted at exactly the mistakes first-time core implementers make. Running it costs an afternoon; standing up a UVM environment costs weeks.
The proportionate version for this project is: seeded pseudo-random stimulus in an ordinary C++ testbench, checked differentially. Use a fixed seed by default so failures reproduce; accept the seed on the command line so a nightly job can sweep; and print the seed in the failure message so a report is actionable. That captures most of the value of randomisation with none of the methodology overhead. Migrate to constrained-random proper only when you can name a bug class that seeded random stimulus provably cannot reach.
The Practical Verification Hierarchy
The techniques above are not alternatives; they are layers, and they have a strict order of adoption. Each layer costs more to build than the one below it and finds bugs the one below it cannot.
flowchart TB
L0["**Layer 0 — it elaborates**<br/>verilator -Wall --lint-only<br/>catches: width mismatches, unused signals,<br/>latch inference, combinational loops<br/>cost: minutes · finds: typos"]
L1["**Layer 1 — directed tests you write**<br/>one module, hand-computed answers<br/>catches: the behaviour you thought about<br/>cost: hours · finds: your implementation mistakes"]
L2["**Layer 2 — assertions in the RTL**<br/>invariants checked on every stimulus, forever<br/>catches: violations from tests written later<br/>cost: minutes each · finds: interaction bugs"]
L3["**Layer 3 — the official suite**<br/>[[The riscv-tests Suite]] rv32ui-p-*, then rv32um, rv32uc<br/>catches: the behaviour you misunderstood<br/>cost: a day of plumbing · finds: your spec misreadings"]
L4["**Layer 4 — differential vs a reference**<br/>[[The Single-Cycle Processor]] or sail-riscv, cycle by cycle<br/>catches: bugs nobody wrote a test for<br/>cost: days · finds: the long tail"]
L5["**Layer 5 — randomised programs + coverage feedback**<br/>riscv-dv class tooling, coverage-driven closure<br/>catches: rare corner interactions<br/>cost: weeks · finds: what remains"]
L0 --> L1 --> L2 --> L3 --> L4 --> L5
L1 -.->|"your tests encode<br/>your misunderstandings"| L3
L3 -.->|"the suite ends;<br/>the design keeps changing"| L4
The verification hierarchy, in adoption order. What it shows: each layer is a strictly larger net at a strictly higher cost, and the two dashed arrows are the reasons you cannot stop early — your own tests share your misconceptions, so an external suite is required; and a fixed suite stops finding new bugs the moment you finish passing it, so a continuous oracle is required after that. The insight to take: the definitely-not-esp32 MOC makes Layer 3 an entire stage (“Stage 4 — Prove It Is Actually a RISC-V”) precisely because it is the layer people skip, and it is the layer that says “expect to fail it, and expect the failures to be in the instructions you were most confident about.”
Layer 0 deserves one sentence of its own because it is nearly free and almost always skipped. verilator --lint-only -Wall runs the front end without generating a model and reports width mismatches, unintended latches, unused and undriven signals, and blocking assignments in sequential blocks. On a design being written by someone learning Verilog it catches real bugs in seconds. Turning warnings into errors in the project Makefile from day one is cheaper than any later measure.
Layer 3 has an important structural property worth understanding before you get there. riscv-tests programs are self-checking in the target’s own instruction set — the example in the repository’s README computes a result, compares it against an expected constant with bne, and branches to RVTEST_FAIL if they differ. The README is admirably blunt about the limit of that design:
The example program contains self-checking code to test the result of the add. However, self-checks rely on correct functioning of the processor instructions used to implement the self check (e.g., the branch) and so cannot be the only testing strategy. (riscv-tests README)
That is the cleanest possible statement of why Layer 4 exists. A test written in the language of the thing being tested is circular exactly where the thing is broken: a core with a broken bne passes every bne-checked test. Differential comparison against an external oracle is the only way out of that circle, which is why the README also specifies a data section that “will be captured at the end of the test to act as a signature […] compared with that from a run on the golden model.”
One more practical detail from the same source: each test targets a test virtual machine (rv32ui = “RV32 user-level, integer only”) and a target environment (p = “virtual memory is disabled, only core 0 boots up”), which is why the file names read rv32ui-p-add. For a Stage-4 core with no MMU and no supervisor mode, rv32ui-p-* is exactly and only the right set — and the README adds a requirement testbenches routinely forget: “Any given test environment for running tests should also include a timeout facility, which will class a test as failing if it does not successfully complete a test within a reasonable time bound.” A hung core must fail, not hang the regression.
Failure Modes and Common Misunderstandings
Two-state simulation hides missing resets — and the flag that unhides them is a runtime option. This is the highest-value thing in this section, and it is measured rather than asserted. Take a counter with an incomplete reset — count is reset, a companion armed flag is not:
module nores (input wire clk, input wire rst, input wire en, output reg [7:0] count); reg armed; always @(posedge clk) begin if (rst) count <= 8'd0; // <-- `armed` missing here else if (en && armed) count <= count + 1'b1; if (en) armed <= 1'b1; endendmodule
Run for ten enabled cycles, the correct answer is 9 (the first cycle is consumed setting armed). But if armed powers up as 1 — as it may on real silicon, and as a four-state simulator would model with X — the answer is 10. Verilator’s manual says --x-initial unique is the default and that it “allows for finding reset bugs”, but adds that you must “use the +verilator+rand+reset+2 runtime option, and seed the runtime random number generator … with +verilator+seed+<value>” (Verilator argument reference). Measuring all four combinations on 5.046:
$ ./Vd # no runtime flagcount after 10 enabled cycles = 9 (expected 9) # ... always 9. Bug invisible.$ for s in 1 2 3 4 5 6; do ./Vd +verilator+seed+$s +verilator+rand+reset+2; donecount after 10 enabled cycles = 9 (expected 9)count after 10 enabled cycles = 10 (expected 9) # <-- bug exposedcount after 10 enabled cycles = 9 (expected 9)count after 10 enabled cycles = 10 (expected 9)count after 10 enabled cycles = 9 (expected 9)count after 10 enabled cycles = 10 (expected 9)$ ./Vx +verilator+seed+1 # built --x-initial unique,count after 10 enabled cycles = 9 (expected 9) # but no runtime flag: still hidden$ ./Vz +verilator+seed+2 +verilator+rand+reset+2 # built --x-initial 0:count after 10 enabled cycles = 9 (expected 9) # runtime flag now inert
The bug appears in three of six seeds — a coin flip per run — and only when the runtime option is present. So: adding --x-initial unique to your Verilator command line and expecting to catch reset bugs does nothing, because it was already the default; the flag that matters is +verilator+rand+reset+2 on the simulation binary, and --x-initial 0 at compile time silently disables it. Put both the seed and +verilator+rand+reset+2 into your regression runner, print the seed on failure, and accept that a passing run at one seed proves less than a passing run at fifty.
Lint is free and catches a class of bug a testbench never will.--lint-only -Wall runs the front end alone. On the counter it took 0.003 s of walltime. On a module with an unintentionally inferred latch it produced:
$ verilator --lint-only -Wall lintbad.v --top-module lintbad%Warning-LATCH: lintbad.v:4:5: Latch inferred for signal 'z' (not all control paths of combinational always assign a value) : ... Suggest use of always_latch for intentional latches 4 | always @* if (a[0]) z = 1'b1; | ^~~~~~ ... For warning description see https://verilator.org/warn/LATCH?v=5.046 ... Use "/* verilator lint_off LATCH */" and lint_on around source to disable this message.%Error: Exiting due to 1 warning(s)
Note that -Wall makes it exit non-zero — the lint step is a test. An inferred latch will never show up as a wrong value in simulation; it shows up as a design that fails timing or behaves differently after FPGA synthesis, which is the worst possible place to discover it (see Timing Closure and Fmax).
Duplicate dump timestamps silently drop trace data. Covered above; the symptom is a waveform that disagrees with the printf log. Verilator warns per occurrence — %Warning: previous dump at t=25, requesting t=25, dump call ignored — but it does not abort, so on a long run the warning scrolls away.
A testbench that never fails. The single most common defect in a testbench is that it cannot fail: the comparison is against a value read from the DUT, the errors counter is never returned, or the loop exits before the interesting cycle. Test your test by planting a bug. The -GBUG=0 / -GBUG=1 pattern above exists for exactly this: a parameterised defect that can be switched on to prove the checker fires. If you cannot make your testbench fail on demand, you do not know that it passes.
Confusing simulated time with cycles. Simulated time is whatever timeInc() made it; cycles are what you counted. Report both in failure messages and reason in cycles. A performance number quoted in simulated time is meaningless without the period.
Checking the wrong side of the clock edge. Reading a registered output before calling eval() with the rising edge gives the previous cycle’s value; reading a combinational output after a clock edge but before the settling eval() gives a stale value. Fix the convention once — “check immediately after the rising-edge eval()” — and apply it everywhere.
Forgetting dut.final().final() runs any SystemVerilog final blocks and flushes model state. Omitting it loses end-of-simulation $display output and can truncate a coverage write.
Assuming a passing simulation means a working FPGA. Verilator models the synthesizable subset in two states with no timing. It cannot tell you that your critical path is 40 ns, that your clock-domain crossing lacks a synchroniser, or that your initial block will not exist in the bitstream. The MOC’s rule stands: simulate to design, synthesize to confirm.
Alternatives and When to Choose Them
The C++-testbench-around-Verilator model is not the only way to drive RTL, and the alternatives have real places.
A Verilog testbench under Icarus Verilog. Write the stimulus in Verilog itself, using initial, always #5 clk = ~clk;, $display, $dumpvars and $finish. Icarus is a four-state, event-driven interpreter, so it handles X and Z properly, supports delays and behavioural constructs Verilator will not, and needs no C++ at all. The same file used in this note ran under both:
$ iverilog -g2012 -o tb_iv tb_self.v && ./tb_ivVCD info: dumpfile self.vcd opened for output.result=98tb_self.v:25: $finish called at 100 (1s)
Choose Icarus for a quick behavioural experiment, for a testbench that must also run on a commercial simulator, or when you specifically need four-state X propagation to hunt an initialisation bug. Do not choose it as the main development simulator for a CPU: it is an interpreter, and the throughput difference is what makes running a full riscv-tests regression on every commit practical or impractical.
Verilator --binary. A middle path: keep the testbench in Verilog, but compile it with Verilator’s timing support so it runs at compiled speed. Good for reusing an existing Verilog testbench. Poor once the testbench needs to load an ELF file, model a memory with realistic latency, or hold a reference implementation.
cocotb. A Python coroutine framework that drives a simulator through VPI/VHPI, including Verilator. The stimulus and checking are written in Python with async/await, which makes complex bus protocols and scoreboards genuinely pleasant, and gives you the whole Python ecosystem for reference models. The cost is a per-signal-access overhead across the language boundary, which matters once you are running millions of cycles.
UVM on a commercial simulator. The industry standard, and out of scope for a hobby project without licences, as discussed above.
Formal property verification. Instead of running stimulus, prove a property holds for all stimulus. SymbiYosys drives open-source model checkers over SystemVerilog assertions, and for narrow, self-contained properties — a FIFO never overflows, a one-hot encoding is always one-hot, an arbiter is fair — a proof is stronger than any number of simulation cycles. Formal is complementary, not a replacement: it excels where the state space is small and the property is crisp, and struggles exactly where a CPU is interesting.
Approach
Language
State model
Speed
Best for
Verilator + C++ testbench
C++
Two-state
Fastest compiled
The default for this project; anything with a software reference model
Verilator --binary
Verilog/SV
Two-state
Compiled
Reusing an existing Verilog testbench
Icarus Verilog
Verilog/SV
Four-state
Interpreted, slow
X/Z behaviour, quick experiments, portability
cocotb
Python
Simulator’s
Bounded by VPI crossings
Protocol-heavy testbenches, rich reference models
UVM + commercial simulator
SV/UVM
Four-state
Fast, licensed
Production ASIC verification
Formal (SymbiYosys)
SVA
Symbolic
N/A — proof
Small crisp invariants, exhaustively
Testbench approaches compared. What it shows: the axis that actually separates these is not speed but where the checker lives — in C++, in Verilog, in Python, or nowhere because a solver is doing the work. The insight to take: rows 1 and 6 are the pair worth combining. Simulation with a golden model finds the bugs you can reach; formal proves the handful of invariants that must hold everywhere. The middle rows are conveniences, not different capabilities.
Uncertain
Verify: cocotb’s current level of Verilator support (which Verilator versions, which features work, and the measured overhead relative to a native C++ testbench). Reason: cocotb was not installed on this machine and its documentation was not fetched during this task, so the description above rests on general knowledge rather than a consulted primary source. To resolve: read the cocotb documentation’s simulator-support matrix and run the same differential ALU testbench under both harnesses to get a real overhead number. #uncertain
Production Notes
Tracing is not free, so do not trace by default. The measurement belongs to Waveform Debugging and is reported there in full, but the headline matters here because it dictates how the test suite is built: on a signal-rich design with high toggle activity, the same 1,000,000-cycle simulation ran at 22.0 MHz simulated with no trace, 1.39 MHz writing a VCD, and 0.175 MHz writing an FST — a 16× and 126× slowdown respectively. The practical consequence is a two-binary build: a fast, untraced binary that the regression suite runs, and a traced binary built from the same sources that you run only on the specific failing test, ideally with tracing gated on a cycle window around the failure. Building --trace into the default target means every regression pays for a waveform nobody will open.
Make the tests runnable by one command, from day one. The complete flow used throughout this note is four lines of shell, and putting it in a Makefile on the first day is what turns “I should check that still works” into something that actually happens:
Parameterise the defect, not the source.-G<name>=<value> “overwrites the given parameter of the top-level module” (Verilator argument reference), which is how the correct and buggy ALU builds in this note came from one file. Keeping a BUG parameter around permanently — defaulting to 0, exercised by a make test-negative target that asserts the suite fails — is a cheap, permanent guard against a testbench that has quietly stopped checking anything.
Fix the seed, print the seed. Every random run in this note used srandom(1) so that a failure at cycle 1 is a failure at cycle 1 on the next run too. A regression that sweeps seeds must print the seed it used in the failure line, and the testbench must accept the seed on the command line so the failure can be replayed exactly. This is the same discipline --x-initial unique requires and for the same reason.
Reference models are worth more than tests. Every hour spent making the single-cycle core a usable oracle — a clean interface for stepping it one instruction, dumping its architectural state, and diffing that state against the pipelined core — pays back across every subsequent stage, because it converts “write a test for this instruction” into “run the existing differential harness on a program that uses it.” The definitely-not-esp32 MOC builds The Single-Cycle Processor at Stage 2 and does not throw it away for exactly this reason.
Timeouts are mandatory. A core that hangs must fail the suite, not the suite’s wall clock. riscv-tests states this as a requirement of any conforming test environment. Bound every testbench by a maximum cycle count and report a distinct TIMEOUT verdict, because “hung” and “wrong answer” have completely different first diagnoses.
Print progress, sparingly. A million-cycle run that prints nothing looks identical to a deadlocked one. A single line every 100,000 cycles carrying the cycle count and the retired program counter costs nothing and turns a mystery into a data point.
See Also
Verilator — the tool this practice is built on: what it compiles, its two-state semantics, its language coverage and its release cadence
Waveform Debugging — the other half of the pair: what to do after a self-checking test fails, and the measured cost of tracing