A new engineer looks at DCRouter, a router you could read in an afternoon, and asks a fair question: it is so small, why not simulate every possible input and be certain? The arithmetic answers in one line. DCRouter holds 811 bits of state. The number of states it could be in has 245 digits. A simulator running for the age of the universe would not visit a measurable fraction of them.
If even a small design cannot be tested exhaustively, what does testing actually achieve?
The obvious answer is "more": more tests, more seeds, more cycles, a bigger compute farm, until every case is covered. That intuition comes from software functions with a handful of inputs, where trying them all is sometimes possible. Hardware is different in two ways. It has state: what a block does this cycle depends on everything it has seen before. And it runs every cycle: each clock edge multiplies the possibilities by every input combination. Both grow exponentially, and exponential growth defeats any amount of compute.
Two numbers bound what exhaustive testing would need (fact M1):
States. A design with k bits of state can be in up to 2^k states. Each extra bit doubles the count.
Input sequences. With i input bits per cycle, there are 2^(i·L) different input sequences of L cycles. Bugs often need a particular sequence, not just a particular state.
Not every state is reachable in practice, and many states behave identically, so real designs are smaller than these bounds suggest. But the bounds are so large that even a tiny reachable fraction is out of reach.
The model counts DCRouter's state bits from its RTL, then asks how long it would take merely to visit every state of designs of growing size, at an illustrative simulation speed of 10,000 cycles per second and emulation speed of 1,000,000, assuming every single cycle reached a new state (which real tests never do).
"""Why exhaustive simulation is impossible: counting states and input sequences.
Part 1 counts DCRouter's state bits from its RTL (FIFO storage and pointers, per-input
packet state, per-output lock and credit state, registers, sleep control). Part 2 asks how
long it would take just to visit every possible state of designs of growing size, at an
illustrative simulation speed of 10,000 cycles per second and emulation speed of 1,000,000,
even if every cycle reached a new state. Part 3 counts input sequences: DCRouter has 119
input bits per cycle (valids, data, lasts, credit returns and the APB inputs), so the number
of distinct 10-cycle input sequences is 2^(119*10).
"""
import math
inventory = { # (bits per copy, copies)
"FIFO storage, 8 x 17 bits": (8 * 17, 4),
"FIFO pointers and count": (3 + 3 + 4, 4),
"per-input packet state": (4 + 5 + 8 + 1 + 2 + 1 + 1, 4),
"per-output lock, owner, rr, credits": (1 + 2 + 2 + 3, 4),
"CTRL fields": (4 + 1 + 1, 1),
"ERR_CNT and PKT_CNT": (8 + 16, 4),
"sleep and idle counter": (1 + 4, 1),
}
state_bits = sum(b * n for b, n in inventory.values())
input_bits = 4 + 64 + 4 + 4 + 1 + 1 + 1 + 8 + 32 # in_vld, in_data, in_last, out_crd, psel, penable, pwrite, paddr, pwdata
SIM, EMU = 1e4, 1e6 # cycles per second (illustrative)
YEAR = 3.15e7 # seconds
print(f"DCRouter state bits: {state_bits} (2^{state_bits} = 10^{state_bits * math.log10(2):.0f} possible states)")
print(f"DCRouter input bits per cycle: {input_bits}")
print("state bits: " + " ".join(f"{b:>7d}" for b in (16, 32, 48, 64, 80, 96)))
print("log10 of states: " + " ".join(f"{b * math.log10(2):>7.1f}" for b in (16, 32, 48, 64, 80, 96)))
print(f"log10 of cycles in a year: simulation {math.log10(SIM * YEAR):.1f}, emulation {math.log10(EMU * YEAR):.1f}")
rows = []
for name, speed in (("simulation, years:", SIM), ("emulation, years: ", EMU)):
logs = [b * math.log10(2) - math.log10(speed * YEAR) for b in (16, 32, 48, 64, 80, 96)]
rows.append(logs)
print(f"{name} " + " ".join(f"{('1e%+.0f' % l):>7s}" for l in logs))
seq_log10 = input_bits * 10 * math.log10(2)
print(f"distinct 10-cycle input sequences: 10^{seq_log10:.0f}")
assert state_bits == 811 and input_bits == 119
assert rows[0][1] > -2.5 and rows[1][3] > 5 # 32 bits: days in simulation; 64 bits: a million years in emulation
print("PASS: even 64 bits of state outlast any emulator, and DCRouter has 811")It prints:
DCRouter state bits: 811 (2^811 = 10^244 possible states)
DCRouter input bits per cycle: 119
state bits: 16 32 48 64 80 96
log10 of states: 4.8 9.6 14.4 19.3 24.1 28.9
log10 of cycles in a year: simulation 11.5, emulation 13.5
simulation, years: 1e-7 1e-2 1e+3 1e+8 1e+13 1e+17
emulation, years: 1e-9 1e-4 1e+1 1e+6 1e+11 1e+15
distinct 10-cycle input sequences: 10^358
PASS: even 64 bits of state outlast any emulator, and DCRouter has 811How to read it: the state count rises in a straight line on this log scale, adding three digits for every ten bits. A year of simulation covers about 10^11.5 cycles, which a 38-bit design already exceeds. A 64-bit counter would take about a million years on an emulator. DCRouter, with 811 bits, is beyond any of these by more than two hundred orders of magnitude, and its input sequences are worse still: 10^358 different ten-cycle sequences.
If trying everything is impossible, verification has to choose what to try, and justify the choice. Every technique in this course is a different answer to "which tiny fraction is worth running?"
Strategy | How it cuts the space | What it costs or risks |
|---|---|---|
Directed tests on risky cases | Engineers pick the cases they believe matter | Only finds bugs someone imagined |
Random and constrained-random sampling | Samples the space broadly and cheaply | Rare corners stay rare (Part 4) |
Coverage | Measures which planned situations the samples reached | Only as good as the plan behind it (Part 6) |
Formal proof | Reasons about every sequence at once, symbolically | Works on blocks, not whole chips (Part 7) |
Hierarchy and abstraction | Verifies small pieces thoroughly, then their composition | Integration bugs live between the pieces (Part 8) |
Risk-based planning | Spends effort where bugs are likely and costly | Depends on judging risk well (Part 9) |
Practice | What it does with the impossibility |
|---|---|
Constrained-random verification (SystemVerilog, fact V1) | Generates millions of legal, varied tests instead of hand-writing a few |
Functional coverage (fact V1) | Replaces "did we try everything?" with "did we reach everything in the plan?" |
Formal property checking (fact V2) | Proves properties of control blocks for every sequence the assumptions allow |
Sign-off on evidence | Accepts a stated residual risk instead of claiming completeness (Part 14) |
A team (illustrative) planned verification of a 16-entry, 4-port arbiter by "running random tests until nothing fails for a week". Nothing failed for a week. The arbiter's bug needed all four ports to request in one cycle while its pointer wrapped, a state the random traffic reached perhaps once a month. A one-line count of the arbiter's state and the probability of that combination would have shown the week proved little, and pointed to either biased stimulus or a formal check of the arbiter, which found the bug in minutes.
No. 2^40 is about 1.1 × 10^12 states, while a year at 10^4 cycles per second is about 3.2 × 10^11 cycles, and real tests revisit states constantly.
Many bugs need a particular order of events across cycles, such as a request arriving the cycle after a reset; the number of sequences grows with every cycle of length, far faster than the number of states.
Rarely: the reachable fraction is smaller than 2^k, but for any real design it is still astronomically large; reachability arguments are what formal tools exploit, not simulation.
States grow as 2^k and input sequences as 2^(i·L): exhaustive simulation is impossible for any real design.
Verification is therefore a choice of which cases to run, and the evidence that the choice was good.
Every technique in this course (random, coverage, formal, planning) is an answer to that choice.