Verification Bridge: cocotb, Verilator and Golden Models

Topics We'll Cover

• A Bridge in Both Directions
• The Design Under Test: an NTT Core
• cocotb in One Page
• Two Golden Models and a Scoreboard
• Transactors: Driving and Sampling Ready/Valid
• Constrained-Random Stimulus
• Functional Coverage, and the Crosses That Matter
• Interactive: Coverage Closure
• A Seeded Bug: Caught or Escaped
• Verilator, Icarus and CI for RTL
• RTL Cycle Counts and a Cycle Model
• Feeding the RTL Back Into the Simulator
• Switching Activity as a Power Proxy
• What to Take Away

A Bridge in Both Directions

An architecture simulator and the RTL describe the same machine at different levels. Each can check the other. The simulator's functional model is the golden model that says what the RTL must compute. The RTL's measured cycle counts say how fast the simulator may assume each unit runs. The LLM Inference Simulators glossary introduces co-simulation. This deck builds both directions for one unit: the NTT that dominates FHE workloads (FHE Accelerator Simulators 01, slide 05).

The code is RTL_CoSim_NTT. Every number on these slides comes from its examples/results.md.

The Design Under Test: an NTT Core

Barrett's quotient estimate is never too large and at most two too small, so the remainder needs up to two correction steps. The second is the subject of most of this deck. A compile-time define seeds a bug there by dropping it:

`ifdef INJECT_BUG
            if (r0 >= q_ext) begin
                r    <= W'(r0 - q_ext);
                corr <= (r0 >= q2_ext) ? 2'd2 : 2'd1;
            end else begin
                r    <= W'(r0);
                corr <= 2'd0;
            end
`else
            if (r0 >= q2_ext) begin
                r    <= W'(r0 - q2_ext);
                corr <= 2'd2;
            end else if (r0 >= q_ext) begin
                r    <= W'(r0 - q_ext);
                corr <= 2'd1;
            end else begin
                r    <= W'(r0);
                corr <= 2'd0;
            end
`endif

All three modules are -Wall lint-clean in Verilator and parse in Icarus. The data memory is a register array with 2P read ports, which is fine for simulation; a chip would bank SRAMs instead, and the cycle counts would not change.

cocotb in One Page

cocotb runs Python coroutines alongside an HDL simulator. A test is an async function that drives signals, and awaits triggers (RisingEdge, ClockCycles, ReadOnly, Timer), letting simulated time pass between them. Background coroutines started with cocotb.start_soon act as clocks and monitors. Deck 06, slide 12 introduces it on a modular adder; here it carries a whole verification environment.

async def monitor():
    nonlocal received
    while True:
        await RisingEdge(dut.clk)
        await ReadOnly()
        if dut.out_valid.value == 1:
            got = (int(dut.x.value), int(dut.y.value), int(dut.out_tag.value), int(dut.corr.value))
            want = expected[received]
            if got != want and len(errors) < 10:
                errors.append(f"txn {received}: got {got}, want {want}")
            received += 1

cocotb.start_soon(monitor())

• Python runner. runner.build() compiles the RTL once per parameter set. runner.test() runs a test module and writes JUnit XML. pytest wraps both (tests/test_rtl.py), so RTL tests sit in the same suite as the model tests.
• Versions. The current cocotb documentation says it supports Verilator 5.036+. Ubuntu 24.04 ships 5.020, so this repo pins cocotb 1.9.2. The testbenches only use APIs common to both versions.
• Read-only phase. After await ReadOnly() every signal has settled for this time step, and writes are illegal until the next edge.

Two Golden Models and a Scoreboard

The functional model is the FHE simulator's own code, so the RTL is checked against the same definition the simulator reasons with. The bit-accurate model mirrors the RTL step by step:

def barrett(a: int, b: int, q: int, w_bits: int, mu: int | None = None) -> tuple[int, int]:
    """(a * b mod q, correction steps), computed exactly as rtl/mod_mul_barrett.sv does."""
    if mu is None:
        mu = barrett_mu(q, w_bits)
    x = a * b
    q3 = ((x >> (w_bits - 1)) * mu) >> (w_bits + 1)
    r0 = (x - q3 * q) & ((1 << (w_bits + 2)) - 1)       # the RTL keeps W + 2 bits
    if r0 >= 2 * q:
        return r0 - 2 * q, 2
    if r0 >= q:
        return r0 - q, 1
    return r0, 0

The scoreboard compares each output in order with the model's prediction. The model also reports the correction count the RTL brings out on a corr port, so a hidden mismatch inside the pipeline shows up even when the final value happens to be right.

Transactors: Driving and Sampling Ready/Valid

A transactor turns transactions (a vector to transform) into pin wiggles and back. The NTT core's streams use ready/valid handshakes: a beat moves on the clock edge when both are high. The transactor drives each cycle's inputs at the falling edge, waits for the read-only phase, and records the handshakes the next rising edge will commit:

while len(out) < n:
    await FallingEdge(d.clk)
    cycle += 1
    send = k < beats and not (rng is not None and rng.random() < p_in_gap)
    if send:
        d.in_data.value = sum(x[k * P + l] << (l * self.W) for l in range(P))
    d.in_valid.value = int(send)
    ready = not (rng is not None and rng.random() < p_out_stall)
    d.out_ready.value = int(ready)
    await ReadOnly()
    if send and d.in_ready.value == 1:
        first_in = cycle if first_in is None else first_in
        last_in = cycle
        k += 1
    if ready and d.out_valid.value == 1:
        v = int(d.out_data.value)
        out.extend((v >> (l * self.W)) & self.mask for l in range(P))
        first_out = cycle if first_out is None else first_out
        last_out = cycle

Constrained-Random Stimulus

Uniform random operands spread evenly over [0, q), but the corners live in tiny regions: 0, 1, q-1, and products large enough to stress the reduction. A constrained-random generator still covers the whole range, but biases the distribution towards the corners:

def _corner(rng: random.Random, q: int) -> int:
    r = rng.random()
    if r < 0.10:
        return rng.choice((0, 1, q - 1, q - 2))
    if r < 0.55:
        return q - 1 - rng.randrange(max(1, q >> 8))      # the top 1/256 of the range
    return rng.randrange(q)


def constrained(rng: random.Random, q: int) -> tuple[int, int, int]:
    """(a, b, w): corner-biased operands and twiddles."""
    return _corner(rng, q), _corner(rng, q), _corner(rng, q)

How often each generator reaches Barrett's second correction, measured over a million draws of the bit-accurate model:

Source: examples/results.md in RTL_CoSim_NTT

For the near prime, just under 2⁵⁰, mu is almost exact and no draw ever needed a second correction. That bin is excluded for that prime, with the reason written down. That is part of coverage closure, not a way around it.

Functional Coverage, and the Crosses That Matter

Functional coverage counts the situations the stimulus created, in named bins, whatever the code coverage says (deck 06). Each butterfly transaction is sampled from the model's view of it:

def sample_butterfly(cov: Coverage, a: int, b: int, w: int, q: int, t: int, corr: int, gap: int) -> None:
    """Sample one butterfly transaction; t = w*b mod q, corr = Barrett correction steps."""
    cov.hit("a_zero", a == 0)
    cov.hit("a_max", a == q - 1)
    cov.hit("b_zero", b == 0)
    cov.hit("b_max", b == q - 1)
    cov.hit("w_one", w == 1)
    cov.hit("w_max", w == q - 1)
    cov.hit("sum_wraps", a + t >= q)
    cov.hit("sum_no_wrap", a + t < q)
    cov.hit("diff_borrows", a < t)
    cov.hit("diff_no_borrow", a >= t)
    cov.hit(f"corr_{corr}")
    # Crosses. A wrong second correction leaves t off by q, which the add/subtract stage
    # hides unless the sum wraps or the difference borrows: only these crosses make a
    # bug in that step observable at the outputs.
    cov.hit("corr_2_x_sum_wraps", corr == 2 and a + t >= q)
    cov.hit("corr_2_x_diff_borrows", corr == 2 and a < t)
    cov.hit("back_to_back", gap == 0)
    cov.hit("after_gap", gap > 0)

Why the crosses. If the second correction is dropped, the product t = w*b mod q comes out as t + q. The add stage computes a + t + q - q, which is right whenever a + t < q, and the subtract stage gives a - t, right whenever a ≥ t. So the error is masked unless the sum wraps or the difference borrows. Hitting corr_2 is not enough. Only the crosses show the stimulus made the bug observable. That was found the hard way, as slide 09 shows.

Interactive: Coverage Closure

Runs the bit-accurate Barrett butterfly in your browser (BigInt arithmetic) on uniform or corner-biased stimulus, and fills the bins as it goes. Compare the rates with the recorded million-draw study below. The browser's random numbers are not seeded, so counts vary from run to run.

A Seeded Bug: Caught or Escaped

Five campaigns on the RTL in Verilator, each with the bit-accurate scoreboard. Two run the INJECT_BUG build, which drops the second correction:

Source: examples/results.md in RTL_CoSim_NTT

• The uniform campaign passed with the bug in. It even reached the second correction once, in the masked region. A green regression is not evidence on its own.
• Coverage showed it before anyone looked at a waveform. The observable crosses were empty, along with the corner bins.
• Constrained stimulus closed coverage and caught the bug with 4,000 transactions. pytest pins both outcomes (tests/test_rtl.py), so a change that weakens the generator fails the build.

Verilator, Icarus and CI for RTL

stage('Lint') {
    steps {
        sh(env.VPATH + 'verilator --lint-only -Wall rtl/*.sv --top-module ntt_core')
        sh(env.VPATH + 'verilator --lint-only -Wall -GP=4 rtl/*.sv --top-module ntt_core')
        sh 'iverilog -g2012 -o /dev/null rtl/*.sv'
    }
}

stage('Model tests') {
    steps {
        sh '.venv/bin/pytest -m "not rtl" --junitxml=pytest-model.xml --cov=ntt_cosim --cov-report=xml:coverage.xml'
        recordCoverage(tools: [[parser: 'COBERTURA', pattern: 'coverage.xml']], sourceCodeRetention: 'LAST_BUILD')
    }
}

stage('RTL tests (Verilator)') {
    steps {
        sh(env.VPATH + "SIM=verilator NIGHTLY=${params.NIGHTLY ? 1 : 0} .venv/bin/pytest -m rtl --junitxml=pytest-verilator.xml")
    }
}

stage('RTL tests (Icarus)') {
    steps {
        sh(env.VPATH + 'SIM=icarus .venv/bin/pytest -m rtl --junitxml=pytest-icarus.xml')
    }
}

stage('Cycle-count gate') {

Cycle counts are deterministic, so the performance gate is exact: any transform that takes one more cycle than ci/cycle_baseline.json fails the build. That catches a change that adds a pipeline stage before it silently costs throughput.

RTL Cycle Counts and a Cycle Model

Each stage issues n/2P butterfly groups, then waits for its last results to be written back before the next stage may read them. The wait is the five-cycle butterfly pipeline plus one cycle to see it is empty:

Source: examples/results.md in RTL_CoSim_NTT

The model matches every measurement exactly, at every size and lane count built, so it can be trusted to extrapolate to n = 2¹⁶, too large to simulate quickly with a register-array memory. More lanes finish sooner but waste a larger share of each stage on the drain: efficiency falls as P grows.

Feeding the RTL Back Into the Simulator

FHE_Accelerator_Sim costs an NTT at ntt_bfly_per_cycle butterflies per cycle: efficiency 1. Derating it by the efficiency this RTL achieves at N = 2¹⁶ needs one more fact: how the 4096 lanes are grouped into cores. The simulator does not say, so several groupings are compared:

Source: examples/results.md in RTL_CoSim_NTT

• The memory-bound baseline barely moves (13.94 to 14.63 ms at worst), because HBM, not the NTT units, sets its pace.
• The optimised algorithm changes verdict. With one 4096-lane core, Min-KS + seeded keys + OTF plaintexts goes from MAC-bound to NTT-bound: the optimisation that removed the memory bottleneck exposes the NTT microarchitecture.
• A ping-pong buffer (load the next transform while computing this one) recovers most of the loss. It is a modelled what-if, not built in this RTL. That is the kind of question a calibrated simulator answers before the RTL is written.

On the NTT-starved small design, every microsecond of NTT time is on the critical path, and the same derating costs up to 26%:

Source: examples/results.md in RTL_CoSim_NTT

Switching Activity as a Power Proxy

Dynamic power is roughly activity × capacitance × V² × f. Before a gate-level netlist exists, toggle counts on the RTL's registers give the activity term and show how strongly power depends on the data (RTL power analysis). The testbench samples the multiplier's pipeline registers and the outputs every cycle:

Source: examples/results.md in RTL_CoSim_NTT

• Random 50-bit data is the worst case, and FHE ciphertexts are uniformly random by design, so the pessimistic number is the right one for this workload.
• A fixed twiddle saves almost nothing here, because w*b still sees random b.
• Limits. Every register bit counts equally. Combinational nets, glitches, clock-tree and memory power are missing. A real flow writes SAIF or VCD activity and runs a power tool on the netlist. The proxy ranks workloads; it does not give watts.

What to Take Away

• Use the simulator's functional model as the RTL's golden model, and a bit-accurate model as the scoreboard for internals.
• Transactors sample handshakes in the cycle they happen, not after the edge that commits them.
• Coverage, not vector counts, says when you are done. Cross the corner with the condition that makes a bug in it observable.
• Seed a bug and check that the testbench catches it. Here uniform stimulus passed with the bug in; constrained stimulus caught it.
• Run two simulators, lint with -Wall, and gate on exact cycle counts in CI.
• Feed measured cycles back through a cycle model the measurements confirm. A derated unit can change the simulator's verdict.

• RTL_CoSim_NTTThe RTL, the testbenches, the models and examples/results.md.
• cocotb documentation and the Verilator manualCheck simulator version support before upgrading either.
• Deck 06: Testing Frameworks for Simulatorscocotb basics, mutation testing and coverage.
• FHE Accelerator Simulators 04: Optical NTT EnginesThe same NTT, computed by optics.
• Interview_SystemVerilogInterview questions on SystemVerilog, UVM and coverage.