Hardware is unforgiving in a way software is not. A bug found after a design ships in a device cannot be patched over the air, and on the way there a subtle timing or crossing bug can hide for a long time and surface rarely. So verification is not a phase at the end, it is the larger part of the work, and every module in this series arrived with a testbench that checked it before it was trusted. This closing page gathers the methods, from the self-checking testbench used throughout to the tools that go further.
The self-checking testbench
The testbench pattern used across this series has one defining property. It never asks a human to read waveforms and judge. It computes the right answer independently and compares, then prints pass or fails the run with a nonzero exit code, so that running the whole suite is a single clean signal. The independent reference is the important part. For the sequence detector it was a sliding window over the input bits, computed a completely different way from the state machine, so the two agreeing is real evidence rather than the same possible mistake made twice. Directed cases pin down the corners a human can name, the reset, the wrap, the full and empty edges, and random stimulus by the thousands covers the combinations a human would never think to enumerate. The debugging earlier in this project made the point sharply, since two of the failures turned out to be bugs in the testbenches rather than the modules, which is exactly why the reference has to be independent and the stimulus thorough.
Driving a simulation from Python with cocotb
Testbenches written in the hardware language are fine for small modules, but for anything with a complex environment it is often easier to drive the simulation from software, where queues, models, and randomization are natural. Cocotb does exactly this. It leaves the design in SystemVerilog and writes the testbench in Python, awaiting clock edges and poking signals as coroutines, so the whole reference model and scoreboard can be ordinary Python. The same dot-product tile from the capstone might be checked like this.
test_dot4.pyimport cocotb
from cocotb.clock import Clock
from cocotb.triggers import RisingEdge
@cocotb.test()
async def dot4_matches_reference(dut):
cocotb.start_soon(Clock(dut.clk, 10, units="ns").start())
dut.rst.value = 1
await RisingEdge(dut.clk)
dut.rst.value = 0
W = 16
pending = [] # reference results, in flight through the pipeline
for _ in range(500):
a = [random_signed(W) for _ in range(4)]
b = [random_signed(W) for _ in range(4)]
dut.a_flat.value = pack(a, W)
dut.b_flat.value = pack(b, W)
dut.in_valid.value = 1
pending.append(sum(ai * bi for ai, bi in zip(a, b)))
await RisingEdge(dut.clk)
if dut.out_valid.value == 1:
assert dut.dot.value.signed_integer == pending.pop(0)
The Python reference, one line summing the products, is obviously correct at a glance, which is the goal. Cocotb runs on top of the same open simulator used throughout this series, so nothing about the design changes, only the language the testbench is written in.
Assertions that watch from the inside
A testbench checks outputs. Assertions check invariants, properties that must hold at every moment, written right beside the logic and evaluated continuously during any simulation. SystemVerilog assertions are the built-in way. A concurrent assertion states a rule about behavior over time, and if the rule is ever broken the simulation reports exactly when and where, often catching a problem cycles before it would have corrupted an output. For a FIFO, two invariants say a great deal.
fifo_assertions.sv// the count must never exceed the depth, and never wrap below zero
assert property (@(posedge clk) disable iff (rst)
count <= DEPTH);
// a push on a full FIFO or a pop on an empty one must never be honored
assert property (@(posedge clk) disable iff (rst)
(full |-> !(wr && !rd)) );
// once the master raises valid it must hold data until the transfer completes
assert property (@(posedge clk) disable iff (rst)
(m_valid && !m_ready) |=> (m_valid && $stable(m_data)) );That last assertion is the AXI-Stream rule from the interfaces page, written as a property a tool can check automatically. Assertions earn their keep most when they ride along in every test, quietly guarding rules the test author was not even thinking about.
Formal, proving instead of sampling
Simulation, however thorough, only samples the input space. It runs the cases you drove and no others. Formal verification takes the same assertions and, instead of trying inputs, mathematically proves that no possible sequence of inputs can ever violate them, or hands back the exact short sequence that does. For a well-scoped module like a FIFO, a synchronizer, or an arbiter, this is within reach of open tools and gives a guarantee simulation cannot, that the property holds for every input, not merely the ones tried. The honest practice is to lean on self-checking simulation for the bulk of a design and to bring formal to the small, tricky, high-stakes blocks where a rare bug would be worst, which are exactly the crossings and the control logic this series spent its care on.
That closes the series. From the lookup table and the flip-flop, up through combinational and sequential logic, state machines, arithmetic, memory, pipelining, timing, crossings, and interfaces, to a matrix-multiply engine, every piece written to be read and checked to be trusted. The runnable source for all of it is in the advanced-fpga-design repository.